1.1 --- a/src/HOL/Tools/meson.ML	Wed Feb 13 10:19:30 2008 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Wed Feb 13 15:14:17 2008 +0100
     1.3 @@ -646,9 +646,13 @@
     1.4  fun negated_asm_of_head th =
     1.5      th RS notEfalse handle THM _ => th RS notEfalse';
     1.6  
     1.7 -(*Converting one clause*)
     1.8 -val make_meta_clause =
     1.9 -  zero_var_indexes o negated_asm_of_head o make_horn resolution_clause_rules;
    1.10 +(*Converting one theorem from a disjunction to a meta-level clause*)
    1.11 +fun make_meta_clause th =
    1.12 +  let val (fth,thaw) = Drule.freeze_thaw_robust th
    1.13 +  in  
    1.14 +      (zero_var_indexes o Thm.varifyT o thaw 0 o 
    1.15 +       negated_asm_of_head o make_horn resolution_clause_rules) fth
    1.16 +  end;
    1.17  
    1.18  fun make_meta_clauses ths =
    1.19      name_thms "MClause#"