src/Pure/Isar/class.ML
changeset 27761 b95e9ba0ca1d
parent 27708 7471449b9695
child 28017 4919bd124a58
     1.1 --- a/src/Pure/Isar/class.ML	Wed Aug 06 13:57:25 2008 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Aug 06 16:41:40 2008 +0200
     1.3 @@ -65,7 +65,7 @@
     1.4  fun prove_interpretation tac prfx_atts expr inst =
     1.5    Locale.interpretation_i I prfx_atts expr inst
     1.6    #> Proof.global_terminal_proof
     1.7 -      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
     1.8 +      (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (tac ctxt), Position.none), NONE)
     1.9    #> ProofContext.theory_of;
    1.10  
    1.11  fun prove_interpretation_in tac after_qed (name, expr) =
    1.12 @@ -367,7 +367,8 @@
    1.13      val no_constraints = map (map_atyps (K (TFree (Name.aT, [])))) constraints;
    1.14      fun add_constraint c T = Sign.add_const_constraint (c, SOME T);
    1.15      val inst = (#inst o the_class_data thy) class;
    1.16 -    val tac = ALLGOALS (ProofContext.fact_tac facts);
    1.17 +    fun tac ctxt = ALLGOALS (ProofContext.fact_tac facts
    1.18 +      ORELSE' (fn n => SELECT_GOAL (Locale.intro_locales_tac false ctxt []) n));
    1.19      val prfx = class_prefix class;
    1.20    in
    1.21      thy