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#"