--- a/src/Pure/Isar/class.ML Wed Aug 06 13:57:25 2008 +0200
+++ b/src/Pure/Isar/class.ML Wed Aug 06 16:41:40 2008 +0200
@@ -65,7 +65,7 @@
fun prove_interpretation tac prfx_atts expr inst =
Locale.interpretation_i I prfx_atts expr inst
#> Proof.global_terminal_proof
- (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
+ (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (tac ctxt), Position.none), NONE)
#> ProofContext.theory_of;
fun prove_interpretation_in tac after_qed (name, expr) =
@@ -367,7 +367,8 @@
val no_constraints = map (map_atyps (K (TFree (Name.aT, [])))) constraints;
fun add_constraint c T = Sign.add_const_constraint (c, SOME T);
val inst = (#inst o the_class_data thy) class;
- val tac = ALLGOALS (ProofContext.fact_tac facts);
+ fun tac ctxt = ALLGOALS (ProofContext.fact_tac facts
+ ORELSE' (fn n => SELECT_GOAL (Locale.intro_locales_tac false ctxt []) n));
val prfx = class_prefix class;
in
thy