--- a/src/HOL/Tools/function_package/pattern_split.ML Thu Sep 21 03:17:51 2006 +0200
+++ b/src/HOL/Tools/function_package/pattern_split.ML Thu Sep 21 12:22:05 2006 +0200
@@ -94,9 +94,6 @@
val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1
val (_, _ $ (_ $ lhs2 $ _)) = dest_all_all eq2
- val _ = print (cterm_of thy eq1)
- val _ = print (cterm_of thy eq2)
-
val substs = pattern_subtract_subst ctx vs lhs1 lhs2
fun instantiate (vs', sigma) =
@@ -105,10 +102,8 @@
in
fold_rev mk_forall (map Free (frees_in_term ctx t) inter vs') t
end
-
- fun prtrm t = let val _ = print (map (cterm_of thy) t) in t end
in
- prtrm (map instantiate substs)
+ map instantiate substs
end