# HG changeset patch
# User krauss
# Date 1161870399 -7200
# Node ID 9e812f9f3a97c6868df6e7e36e6e6963f594c114
# Parent  b6ab939147eb03cb31a4f581b23488af5bbad918
Removed debugging output

diff -r b6ab939147eb -r 9e812f9f3a97 src/HOL/Tools/function_package/context_tree.ML
--- a/src/HOL/Tools/function_package/context_tree.ML	Thu Oct 26 15:16:31 2006 +0200
+++ b/src/HOL/Tools/function_package/context_tree.ML	Thu Oct 26 15:46:39 2006 +0200
@@ -86,7 +86,6 @@
 fun find_cong_rule ctx fvar h ((r,dep)::rs) t =
     (let
        val thy = ProofContext.theory_of ctx
-       val r = print (zero_var_indexes r)
 
        val tt' = Logic.mk_equals (Pattern.rewrite_term thy [(Free fvar, h)] [] t, t)
        val (c, subs) = (concl_of r, prems_of r)
diff -r b6ab939147eb -r 9e812f9f3a97 src/HOL/Tools/function_package/inductive_wrap.ML
--- a/src/HOL/Tools/function_package/inductive_wrap.ML	Thu Oct 26 15:16:31 2006 +0200
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Thu Oct 26 15:46:39 2006 +0200
@@ -34,7 +34,7 @@
 
 fun requantify ctxt lfix (qs, t) thm =
     let
-      val thy = theory_of_thm (print thm)
+      val thy = theory_of_thm thm
       val frees = frees_in_term ctxt t 
                                   |> remove (op =) lfix
       val vars = Term.add_vars (prop_of thm) [] |> rev