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;