--- a/src/Pure/IsaPlanner/term_lib.ML Wed Nov 16 17:45:29 2005 +0100
+++ b/src/Pure/IsaPlanner/term_lib.ML Wed Nov 16 17:45:30 2005 +0100
@@ -141,7 +141,7 @@
(* Higher order matching with exception handled *)
(* returns optional instantiation *)
fun clean_match thy (a as (pat, t)) =
- let val (tyenv, tenv) = Pattern.match thy a
+ let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
in SOME (Vartab.dest tyenv, Vartab.dest tenv)
end handle Pattern.MATCH => NONE;
(* Higher order unification with exception handled, return the instantiations *)