diff --git a/src/Refinements/CstrAll.class.st b/src/Refinements/CstrAll.class.st
index f3e9e3f37..5f515522d 100644
--- a/src/Refinements/CstrAll.class.st
+++ b/src/Refinements/CstrAll.class.st
@@ -17,7 +17,17 @@ CstrAll >> doElim: bss var: k [
 ]
 
 { #category : #logic }
-CstrAll >> goS1: kve _: env _: __ _: be [
+CstrAll >> goScope: k [
+	| pred c1 |
+	c1 := p.
+	pred := bind p.
+	^(pred pKVars includes: k)
+		ifTrue: [ Either right: self ]
+		ifFalse: [ c1 goScope: k ]
+]
+
+{ #category : #logic }
+CstrAll >> goS′: kve _: env _: __ _: be [
 "
 goS' kve env _   be (H.All b c)  = (be'', subcs)
   where
@@ -32,20 +42,10 @@ goS' kve env _   be (H.All b c)  = (be'', subcs)
 	bId := bId_be1 key.
 	be1 := bId_be1 value.
 	env1 := env insert: bId.
-	be2_subcs := p goS1: kve _: env1 _: bSR _: be1.
+	be2_subcs := p goS′: kve _: env1 _: bSR _: be1.
 	^be2_subcs
 ]
 
-{ #category : #logic }
-CstrAll >> goScope: k [
-	| pred c1 |
-	c1 := p.
-	pred := bind p.
-	^(pred pKVars includes: k)
-		ifTrue: [ Either right: self ]
-		ifFalse: [ c1 goScope: k ]
-]
-
 { #category : #logic }
 CstrAll >> isNNF [ 
 	^ self p isNNF
diff --git a/src/Refinements/CstrAnd.class.st b/src/Refinements/CstrAnd.class.st
index 1757dc481..416d61831 100644
--- a/src/Refinements/CstrAnd.class.st
+++ b/src/Refinements/CstrAnd.class.st
@@ -55,14 +55,6 @@ CstrAnd >> flatten [
 	^CstrAnd of: flatConjuncts
 ]
 
-{ #category : #logic }
-CstrAnd >> goS1: kve _: env _: aSortedReft _: be [
-	| cs be1_subcss |
-	cs := self conjuncts.
-	be1_subcss := cs colject: be into: [ :beSoFar :conjunct | conjunct goS1: kve _: env _: aSortedReft _: beSoFar ].
-	^be1_subcss key -> be1_subcss value flattened
-]
-
 { #category : #logic }
 CstrAnd >> goScope: k [
 	| scopes rights |
@@ -73,6 +65,14 @@ CstrAnd >> goScope: k [
  ^Either right: self "but if kvar appear in multiple chlidren, this is the lca"
 ]
 
+{ #category : #logic }
+CstrAnd >> goS′: kve _: env _: aSortedReft _: be [
+	| cs be1_subcss |
+	cs := self conjuncts.
+	be1_subcss := cs colject: be into: [ :beSoFar :conjunct | conjunct goS′: kve _: env _: aSortedReft _: beSoFar ].
+	^be1_subcss key -> be1_subcss value flattened
+]
+
 { #category : #logic }
 CstrAnd >> isNNF [ 
 	^ self conjuncts allSatisfy: [ :conjunct | conjunct isNNF ]
diff --git a/src/Refinements/CstrAny.class.st b/src/Refinements/CstrAny.class.st
index 9dc32e1ee..bb5aba415 100644
--- a/src/Refinements/CstrAny.class.st
+++ b/src/Refinements/CstrAny.class.st
@@ -5,24 +5,24 @@ Class {
 }
 
 { #category : #logic }
-CstrAny >> goS1: kve _: env _: lhs _: be [
+CstrAny >> goScope: k [
+	self shouldNotImplement "any should not appear after poke"
+]
+
+{ #category : #logic }
+CstrAny >> goS′: kve _: env _: lhs _: be [
 	| bSR bId_be1 bId be1 env1 be2_subcs be2 subcs |
 	bSR := HornQuery bindSortedReft_kve: kve bind: bind.
 	bId_be1 := be insertVar: bind x sort: bSR.
 	bId := bId_be1 key.
 	be1 := bId_be1 value.
 	env1 := env insert: bId.
-	be2_subcs := p goS1: kve _: env1 _: bSR _: be1.
+	be2_subcs := p goS′: kve _: env1 _: bSR _: be1.
 	be2 := be2_subcs key.
 	subcs := be2_subcs value.
 	^be2 -> ({ Either left: bId }, subcs)
 ]
 
-{ #category : #logic }
-CstrAny >> goScope: k [
-	self shouldNotImplement "any should not appear after poke"
-]
-
 { #category : #logic }
 CstrAny >> isNNF [ 
 	^ false
diff --git a/src/Refinements/CstrHead.class.st b/src/Refinements/CstrHead.class.st
index 86f0b73d5..642f8e84d 100644
--- a/src/Refinements/CstrHead.class.st
+++ b/src/Refinements/CstrHead.class.st
@@ -40,7 +40,13 @@ CstrHead >> flatten [
 ]
 
 { #category : #'as yet unclassified' }
-CstrHead >> goS1: kve _: env _: lhs _: be [
+CstrHead >> goScope: k [ 
+	((pred isKindOf: RefVarApp) and: [ pred var = k ]) ifTrue: [ ^Either right: self ].
+	^Either left: #l
+]
+
+{ #category : #'as yet unclassified' }
+CstrHead >> goS′: kve _: env _: lhs _: be [
 	| rhs subc |
 	rhs := lhs updSortedReft_kve: kve p: self pred.
 	subc := SubC new
@@ -51,12 +57,6 @@ CstrHead >> goS1: kve _: env _: lhs _: be [
 	^be -> { Either right: subc }
 ]
 
-{ #category : #'as yet unclassified' }
-CstrHead >> goScope: k [ 
-	((pred isKindOf: RefVarApp) and: [ pred var = k ]) ifTrue: [ ^Either right: self ].
-	^Either left: #l
-]
-
 { #category : #logic }
 CstrHead >> isNNF [ 
 	^ true
diff --git a/src/Refinements/HCstr.class.st b/src/Refinements/HCstr.class.st
index 546b578ee..87a54b324 100644
--- a/src/Refinements/HCstr.class.st
+++ b/src/Refinements/HCstr.class.st
@@ -111,19 +111,19 @@ HCstr >> flatten [
 	self subclassResponsibility
 ]
 
+{ #category : #logic }
+HCstr >> goScope: k [
+	self subclassResponsibility
+]
+
 { #category : #'as yet unclassified' }
-HCstr >> goS1: aCollection _: anIBindEnv _: aSortedReft _: aBindEnv [
+HCstr >> goS′: aCollection _: anIBindEnv _: aSortedReft _: aBindEnv [
 	"goS' :: KVEnv a -> F.IBindEnv -> F.SortedReft -> F.BindEnv -> H.Cstr a
     -> (F.BindEnv, [Either F.BindId (F.SubC a)])
 	cf. various forms of goS' in Horn/Info.hs"
 	self subclassResponsibility 
 ]
 
-{ #category : #logic }
-HCstr >> goScope: k [
-	self subclassResponsibility
-]
-
 { #category : #GT }
 HCstr >> gtInspectorShowIn: composite [
 	<gtInspectorPresentationOrder: 51>
diff --git a/src/Refinements/HornQuery.class.st b/src/Refinements/HornQuery.class.st
index 75e4464ee..a837dea95 100644
--- a/src/Refinements/HornQuery.class.st
+++ b/src/Refinements/HornQuery.class.st
@@ -68,7 +68,7 @@ goS :: KVEnv a -> F.IBindEnv -> F.SortedReft -> F.BindEnv -> H.Cstr a
     -> (F.BindEnv, [F.BindId], [F.SubC a])
 "
 	| be1_ecs mEbs_subcs |
-	be1_ecs := aCstr goS1: kvEnv _: iBindEnv _: lhs _: aBindEnv.
+	be1_ecs := aCstr goS′: kvEnv _: iBindEnv _: lhs _: aBindEnv.
 	mEbs_subcs := be1_ecs value partitionEithers.
 	^{ be1_ecs key. mEbs_subcs key. mEbs_subcs value. }
 ]