src/Pure/Isar/attrib.ML
changeset 45375 7fe19930dfc9
parent 44069 d7c7ec248ef0
child 45390 e29521ef9059
     1.1 --- a/src/Pure/Isar/attrib.ML	Sun Nov 06 21:17:45 2011 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sun Nov 06 21:51:46 2011 +0100
     1.3 @@ -149,8 +149,9 @@
     1.4    thm structure.*)
     1.5  
     1.6  fun crude_closure ctxt src =
     1.7 - (try (fn () => attribute_i (Proof_Context.theory_of ctxt) src
     1.8 -    (Context.Proof ctxt, Drule.asm_rl)) ();
     1.9 + (try (fn () =>
    1.10 +    Thm.apply_attribute (attribute_i (Proof_Context.theory_of ctxt) src)
    1.11 +      (Context.Proof ctxt, Drule.asm_rl)) ();
    1.12    Args.closure src);
    1.13  
    1.14  
    1.15 @@ -198,7 +199,8 @@
    1.16      Parse.$$$ "[" |-- Args.attribs (intern thy) --| Parse.$$$ "]" >> (fn srcs =>
    1.17        let
    1.18          val atts = map (attribute_i thy) srcs;
    1.19 -        val (context', th') = Library.apply atts (context, Drule.dummy_thm);
    1.20 +        val (context', th') =
    1.21 +          Library.apply (map Thm.apply_attribute atts) (context, Drule.dummy_thm);
    1.22        in (context', pick "" [th']) end)
    1.23      ||
    1.24      (Scan.ahead Args.alt_name -- Args.named_fact get_fact
    1.25 @@ -210,7 +212,8 @@
    1.26        let
    1.27          val ths = Facts.select thmref fact;
    1.28          val atts = map (attribute_i thy) srcs;
    1.29 -        val (context', ths') = Library.foldl_map (Library.apply atts) (context, ths);
    1.30 +        val (context', ths') =
    1.31 +          Library.foldl_map (Library.apply (map Thm.apply_attribute atts)) (context, ths);
    1.32        in (context', pick name ths') end)
    1.33    end);
    1.34  
    1.35 @@ -247,7 +250,9 @@
    1.36  
    1.37  (* rename_abs *)
    1.38  
    1.39 -fun rename_abs x = (Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars')) x;
    1.40 +val rename_abs =
    1.41 +  Scan.repeat (Args.maybe Args.name)
    1.42 +  >> (fn args => Thm.rule_attribute (K (Drule.rename_bvars' args)));
    1.43  
    1.44  
    1.45  (* unfold / fold definitions *)
    1.46 @@ -269,18 +274,12 @@
    1.47  
    1.48  (* case names *)
    1.49  
    1.50 -fun hname NONE = Rule_Cases.case_hypsN
    1.51 -  | hname (SOME n) = n;
    1.52 -
    1.53 -fun case_names cs =
    1.54 -  Rule_Cases.case_names (map fst cs) #>
    1.55 -  Rule_Cases.cases_hyp_names (map (map hname o snd) cs);
    1.56 -
    1.57 -val hnamesP =
    1.58 -  Scan.optional
    1.59 -    (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") [];
    1.60 -
    1.61 -fun case_namesP x = Scan.lift (Scan.repeat1 (Args.name -- hnamesP)) x;
    1.62 +val case_names =
    1.63 +  Scan.repeat1 (Args.name --
    1.64 +    Scan.optional (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") []) >>
    1.65 +  (fn cs =>
    1.66 +    Rule_Cases.cases_hyp_names (map fst cs)
    1.67 +      (map (map (the_default Rule_Cases.case_hypsN) o snd) cs));
    1.68  
    1.69  
    1.70  (* misc rules *)
    1.71 @@ -316,8 +315,7 @@
    1.72      "number of consumed facts" #>
    1.73    setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
    1.74      "number of equality constraints" #>
    1.75 -  setup (Binding.name "case_names") (case_namesP >> case_names)
    1.76 -    "named rule cases" #>
    1.77 +  setup (Binding.name "case_names") (Scan.lift case_names) "named rule cases" #>
    1.78    setup (Binding.name "case_conclusion")
    1.79      (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
    1.80      "named conclusion of rule cases" #>