# HG changeset patch
# User paulson
# Date 1202912057 -3600
# Node ID 19df083a2bbf25ff072753b7ddbccef596037b58
# Parent  d80a49f51b9462e439bf0d7bb7b246d15b6b87d0
make_meta_clause bugfix: now works for higher-order clauses like LeastI_ex

diff -r d80a49f51b94 -r 19df083a2bbf src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Wed Feb 13 10:19:30 2008 +0100
+++ b/src/HOL/Tools/meson.ML	Wed Feb 13 15:14:17 2008 +0100
@@ -646,9 +646,13 @@
 fun negated_asm_of_head th =
     th RS notEfalse handle THM _ => th RS notEfalse';
 
-(*Converting one clause*)
-val make_meta_clause =
-  zero_var_indexes o negated_asm_of_head o make_horn resolution_clause_rules;
+(*Converting one theorem from a disjunction to a meta-level clause*)
+fun make_meta_clause th =
+  let val (fth,thaw) = Drule.freeze_thaw_robust th
+  in  
+      (zero_var_indexes o Thm.varifyT o thaw 0 o 
+       negated_asm_of_head o make_horn resolution_clause_rules) fth
+  end;
 
 fun make_meta_clauses ths =
     name_thms "MClause#"