1.1 --- a/src/HOL/ex/Meson_Test.thy	Mon Jul 25 14:10:12 2011 +0200
     1.2 +++ b/src/HOL/ex/Meson_Test.thy	Mon Jul 25 14:10:12 2011 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4    below and constants declared in HOL!
     1.5  *}
     1.6  
     1.7 -hide_const (open) implies union inter subset sum quotient 
     1.8 +hide_const (open) implies union inter subset sum quotient
     1.9  
    1.10  text {*
    1.11    Test data for the MESON proof procedure
    1.12 @@ -31,7 +31,7 @@
    1.13    apply (tactic {* cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1) *})
    1.14    ML_val {*
    1.15      val [_, sko25] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal})));
    1.16 -    val clauses25 = Meson.make_clauses [sko25];   (*7 clauses*)
    1.17 +    val clauses25 = Meson.make_clauses @{context} [sko25];   (*7 clauses*)
    1.18      val horns25 = Meson.make_horns clauses25;     (*16 Horn clauses*)
    1.19      val go25 :: _ = Meson.gocls clauses25;
    1.20  
    1.21 @@ -52,7 +52,7 @@
    1.22    apply (tactic {* cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1) *})
    1.23    ML_val {*
    1.24      val [_, sko26] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal})));
    1.25 -    val clauses26 = Meson.make_clauses [sko26];                   (*9 clauses*)
    1.26 +    val clauses26 = Meson.make_clauses @{context} [sko26];                   (*9 clauses*)
    1.27      val horns26 = Meson.make_horns clauses26;                     (*24 Horn clauses*)
    1.28      val go26 :: _ = Meson.gocls clauses26;
    1.29  
    1.30 @@ -74,7 +74,7 @@
    1.31    apply (tactic {* cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1) *})
    1.32    ML_val {*
    1.33      val [_, sko43] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal})));
    1.34 -    val clauses43 = Meson.make_clauses [sko43];   (*6*)
    1.35 +    val clauses43 = Meson.make_clauses @{context} [sko43];   (*6*)
    1.36      val horns43 = Meson.make_horns clauses43;     (*16*)
    1.37      val go43 :: _ = Meson.gocls clauses43;
    1.38