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/res_axioms.ML
changeset 33832 cff42395c246
parent 33522 737589bb9bb8
child 35568 8fbbfc39508f 
--- a/src/HOL/Tools/res_axioms.ML	Sat Nov 21 14:03:36 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Sat Nov 21 15:49:29 2009 +0100
@@ -29,8 +29,7 @@
 val trace = Unsynchronized.ref false;
 fun trace_msg msg = if ! trace then tracing (msg ()) else ();
 
-(* FIXME legacy *)
-fun freeze_thm th = #1 (Drule.freeze_thaw th);
+fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th);
 
 fun type_has_empty_sort (TFree (_, [])) = true
   | type_has_empty_sort (TVar (_, [])) = true
isabelle