# HG changeset patch
# User blanchet
# Date 1311595812 -7200
# Node ID 31945a5034b7362a26ec8ed2fd72c22cb33f2d6c
# Parent  9338aa218f09ff7be6ec2fba955628483207fd0a
make compile

diff -r 9338aa218f09 -r 31945a5034b7 src/HOL/ex/Meson_Test.thy
--- a/src/HOL/ex/Meson_Test.thy	Mon Jul 25 14:10:12 2011 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Mon Jul 25 14:10:12 2011 +0200
@@ -10,7 +10,7 @@
   below and constants declared in HOL!
 *}
 
-hide_const (open) implies union inter subset sum quotient 
+hide_const (open) implies union inter subset sum quotient
 
 text {*
   Test data for the MESON proof procedure
@@ -31,7 +31,7 @@
   apply (tactic {* cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1) *})
   ML_val {*
     val [_, sko25] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal})));
-    val clauses25 = Meson.make_clauses [sko25];   (*7 clauses*)
+    val clauses25 = Meson.make_clauses @{context} [sko25];   (*7 clauses*)
     val horns25 = Meson.make_horns clauses25;     (*16 Horn clauses*)
     val go25 :: _ = Meson.gocls clauses25;
 
@@ -52,7 +52,7 @@
   apply (tactic {* cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1) *})
   ML_val {*
     val [_, sko26] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal})));
-    val clauses26 = Meson.make_clauses [sko26];                   (*9 clauses*)
+    val clauses26 = Meson.make_clauses @{context} [sko26];                   (*9 clauses*)
     val horns26 = Meson.make_horns clauses26;                     (*24 Horn clauses*)
     val go26 :: _ = Meson.gocls clauses26;
 
@@ -74,7 +74,7 @@
   apply (tactic {* cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1) *})
   ML_val {*
     val [_, sko43] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal})));
-    val clauses43 = Meson.make_clauses [sko43];   (*6*)
+    val clauses43 = Meson.make_clauses @{context} [sko43];   (*6*)
     val horns43 = Meson.make_horns clauses43;     (*16*)
     val go43 :: _ = Meson.gocls clauses43;