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.
updated Misc_Legacy.freeze_thaw;
authorwenzelm
Mon, 19 Mar 2012 21:25:15 +0100
changeset 47024 6c2b7b0421b5
parent 47023 c7a89ecbc71e
child 47025 b2b8ae61d6ad
updated Misc_Legacy.freeze_thaw;
src/HOL/Import/shuffler.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Import/shuffler.ML	Mon Mar 19 21:16:19 2012 +0100
+++ b/src/HOL/Import/shuffler.ML	Mon Mar 19 21:25:15 2012 +0100
@@ -231,7 +231,7 @@
 fun eta_contract thy _ origt =
     let
         val (typet,Tinst) = freeze_thaw_term origt
-        val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet))
+        val (init,thaw) = Misc_Legacy.freeze_thaw (Thm.reflexive (cterm_of thy typet))
         val final = inst_tfrees thy Tinst o thaw
         val t = #1 (Logic.dest_equals (prop_of init))
         val _ =
@@ -282,7 +282,7 @@
 fun eta_expand thy _ origt =
     let
         val (typet,Tinst) = freeze_thaw_term origt
-        val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet))
+        val (init,thaw) = Misc_Legacy.freeze_thaw (Thm.reflexive (cterm_of thy typet))
         val final = inst_tfrees thy Tinst o thaw
         val t = #1 (Logic.dest_equals (prop_of init))
         val _ =
isabelle