src/Pure/more_unify.ML
changeset 63615 d786d54efc70
parent 59787 6e2a20486897
child 74280 7466b17b0820
--- a/src/Pure/more_unify.ML	Fri Aug 05 20:17:27 2016 +0200
+++ b/src/Pure/more_unify.ML	Fri Aug 05 20:26:13 2016 +0200
@@ -21,7 +21,7 @@
   handle Pattern.MATCH => Seq.empty;
 
 (*General matching -- keep variables disjoint*)
-fun matchers _ [] = Seq.single (Envir.empty ~1)
+fun matchers _ [] = Seq.single Envir.init
   | matchers context pairs =
       let
         val thy = Context.theory_of context;