src/Pure/Isar/locale.ML
changeset 36093 0880493627ca
parent 36091 055934ed89b0
child 36094 eb1cc37bc8db
     1.1 --- a/src/Pure/Isar/locale.ML	Mon Feb 15 01:27:06 2010 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Mon Feb 15 01:34:08 2010 +0100
     1.3 @@ -566,15 +566,22 @@
     1.4  
     1.5  
     1.6  (* Tactic *)
     1.7 +fun intros_tac intros facts =
     1.8 +  (TRYALL (Method.insert_tac facts THEN'
     1.9 +      REPEAT_ALL_NEW (resolve_tac intros)) |> CHANGED)
    1.10 +    THEN Tactic.distinct_subgoals_tac;
    1.11  
    1.12 -fun intro_locales_tac eager ctxt =
    1.13 -  Method.intros_tac
    1.14 +fun gen_intro_locales_tac intros_tac eager ctxt =
    1.15 +  intros_tac
    1.16      (get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else []));
    1.17  
    1.18 +val intro_locales_tac = gen_intro_locales_tac Method.intros_tac;
    1.19 +val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
    1.20 +
    1.21  val _ = Context.>> (Context.map_theory
    1.22 - (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o intro_locales_tac false))
    1.23 + (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
    1.24      "back-chain introduction rules of locales without unfolding predicates" #>
    1.25 -  Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o intro_locales_tac true))
    1.26 +  Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
    1.27      "back-chain all introduction rules of locales"));
    1.28  
    1.29  end;