Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/function_package/inductive_wrap.ML
changeset 21105 9e812f9f3a97
parent 21051 c49467a9c1e1
child 21237 b803f9870e97 
--- 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