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