src/Pure/Isar/attrib.ML
changeset 26336 a0e2b706ce73
parent 25983 111d2ed164f4
child 26345 f70620a4cf81
     1.1 --- a/src/Pure/Isar/attrib.ML	Wed Mar 19 18:15:25 2008 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Wed Mar 19 22:27:57 2008 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4    val pretty_attribs: Proof.context -> src list -> Pretty.T list
     1.5    val attribute: theory -> src -> attribute
     1.6    val attribute_i: theory -> src -> attribute
     1.7 -  val eval_thms: Proof.context -> (thmref * src list) list -> thm list
     1.8 +  val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
     1.9    val map_specs: ('a -> 'att) ->
    1.10      (('c * 'a list) * 'd) list -> (('c * 'att list) * 'd) list
    1.11    val map_facts: ('a -> 'att) ->
    1.12 @@ -157,34 +157,36 @@
    1.13  
    1.14  local
    1.15  
    1.16 -val get_thms = Context.cases PureThy.get_thms ProofContext.get_thms;
    1.17 -
    1.18  val fact_name = Args.internal_fact >> K "<fact>" || Args.name;
    1.19  
    1.20 -fun gen_thm pick = Scan.depend (fn st =>
    1.21 -  Args.$$$ "[" |-- Args.attribs (intern (Context.theory_of st)) --| Args.$$$ "]"
    1.22 -    >> (fn srcs =>
    1.23 +fun gen_thm pick = Scan.depend (fn context =>
    1.24 +  let
    1.25 +    val thy = Context.theory_of context;
    1.26 +    val get = Context.cases PureThy.get_thms ProofContext.get_thms context;
    1.27 +    fun get_fact s = get (Facts.Fact s);
    1.28 +    fun get_named s = get (Facts.Named (s, NONE));
    1.29 +  in
    1.30 +    Args.$$$ "[" |-- Args.attribs (intern thy) --| Args.$$$ "]" >> (fn srcs =>
    1.31        let
    1.32 -        val atts = map (attribute_i (Context.theory_of st)) srcs;
    1.33 -        val (st', th') = Library.apply atts (st, Drule.dummy_thm);
    1.34 -      in (st', pick "" [th']) end) ||
    1.35 -  (Scan.ahead Args.alt_name -- Args.named_fact (get_thms st o Fact)
    1.36 -    >> (fn (s, fact) => ("", Fact s, fact)) ||
    1.37 -  Scan.ahead fact_name -- Args.named_fact (get_thms st o Name) -- Args.thm_sel
    1.38 -    >> (fn ((name, fact), sel) => (name, NameSelection (name, sel), fact)) ||
    1.39 -  Scan.ahead fact_name -- Args.named_fact (get_thms st o Name)
    1.40 -    >> (fn (name, fact) => (name, Name name, fact)))
    1.41 -  -- Args.opt_attribs (intern (Context.theory_of st))
    1.42 -  >> (fn ((name, thmref, fact), srcs) =>
    1.43 -    let
    1.44 -      val ths = PureThy.select_thm thmref fact;
    1.45 -      val atts = map (attribute_i (Context.theory_of st)) srcs;
    1.46 -      val (st', ths') = foldl_map (Library.apply atts) (st, ths);
    1.47 -    in (st', pick name ths') end));
    1.48 +        val atts = map (attribute_i thy) srcs;
    1.49 +        val (context', th') = Library.apply atts (context, Drule.dummy_thm);
    1.50 +      in (context', pick "" [th']) end)
    1.51 +    ||
    1.52 +    (Scan.ahead Args.alt_name -- Args.named_fact get_fact
    1.53 +      >> (fn (s, fact) => ("", Facts.Fact s, fact))
    1.54 +    || Scan.ahead fact_name -- Args.named_fact get_named -- Scan.option Args.thm_sel
    1.55 +      >> (fn ((name, fact), sel) => (name, Facts.Named (name, sel), fact)))
    1.56 +    -- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) =>
    1.57 +      let
    1.58 +        val ths = Facts.select thmref fact;
    1.59 +        val atts = map (attribute_i thy) srcs;
    1.60 +        val (context', ths') = foldl_map (Library.apply atts) (context, ths);
    1.61 +      in (context', pick name ths') end)
    1.62 +  end);
    1.63  
    1.64  in
    1.65  
    1.66 -val thm = gen_thm PureThy.single_thm;
    1.67 +val thm = gen_thm Facts.the_single;
    1.68  val multi_thm = gen_thm (K I);
    1.69  val thms = Scan.repeat multi_thm >> flat;
    1.70