Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Removed debugging output
authorkrauss
Thu, 26 Oct 2006 15:46:39 +0200
changeset 21105 9e812f9f3a97
parent 21104 b6ab939147eb
child 21106 51599a81b308
Removed debugging output
src/HOL/Tools/function_package/context_tree.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/function_package/inductive_wrap.ML file | annotate | diff | comparison | revisions 
--- 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)
--- 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
isabelle