src/HOL/Tools/Meson/meson.ML
changeset 47022 8eac39af4ec0
parent 46904 f30e941b4512
child 47035 5248fae40f09
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Mon Mar 19 20:32:57 2012 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Mon Mar 19 21:10:33 2012 +0100
     1.3 @@ -752,7 +752,7 @@
     1.4  
     1.5  (*Converting one theorem from a disjunction to a meta-level clause*)
     1.6  fun make_meta_clause th =
     1.7 -  let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th
     1.8 +  let val (fth,thaw) = Misc_Legacy.freeze_thaw_robust th
     1.9    in  
    1.10        (zero_var_indexes o Thm.varifyT_global o thaw 0 o 
    1.11         negated_asm_of_head o make_horn resolution_clause_rules) fth