src/Pure/more_unify.ML
changeset 59787 6e2a20486897
parent 59026 30b8a5825a9c
child 63615 d786d54efc70
     1.1 --- a/src/Pure/more_unify.ML	Mon Mar 23 17:07:43 2015 +0100
     1.2 +++ b/src/Pure/more_unify.ML	Mon Mar 23 19:43:03 2015 +0100
     1.3 @@ -28,7 +28,7 @@
     1.4  
     1.5          val maxidx = fold (Term.maxidx_term o #2) pairs ~1;
     1.6          val offset = maxidx + 1;
     1.7 -        val pairs' = map (apfst (Logic.incr_indexes ([], offset))) pairs;
     1.8 +        val pairs' = map (apfst (Logic.incr_indexes ([], [], offset))) pairs;
     1.9          val maxidx' = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) pairs' ~1;
    1.10  
    1.11          val pat_tvars = fold (Term.add_tvars o #1) pairs' [];