src/Pure/Pure.thy
changeset 63352 4eaf35781b23
parent 63342 49fa6aaa4529
child 63434 c956d995bec6
     1.1 --- a/src/Pure/Pure.thy	Wed Jun 22 16:04:03 2016 +0200
     1.2 +++ b/src/Pure/Pure.thy	Thu Jun 23 11:01:14 2016 +0200
     1.3 @@ -408,14 +408,14 @@
     1.4    Parse_Spec.long_statement_keyword;
     1.5  
     1.6  val long_statement =
     1.7 -  Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Attrib.empty_binding --
     1.8 +  Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Binding.empty_atts --
     1.9    Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement
    1.10      >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl));
    1.11  
    1.12  val short_statement =
    1.13    Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
    1.14      >> (fn ((shows, assumes), fixes) =>
    1.15 -      (false, Attrib.empty_binding, [], [Element.Fixes fixes, Element.Assumes assumes],
    1.16 +      (false, Binding.empty_atts, [], [Element.Fixes fixes, Element.Assumes assumes],
    1.17          Element.Shows shows));
    1.18  
    1.19  fun theorem spec schematic descr =
    1.20 @@ -444,7 +444,7 @@
    1.21    Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
    1.22      (Parse.and_list1 Parse.thms1 -- Parse.for_fixes
    1.23        >> (fn (facts, fixes) =>
    1.24 -          #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
    1.25 +          #2 oo Specification.theorems_cmd "" [(Binding.empty_atts, flat facts)] fixes));
    1.26  
    1.27  val _ =
    1.28    Outer_Syntax.local_theory @{command_keyword named_theorems}
    1.29 @@ -915,7 +915,7 @@
    1.30  
    1.31  val opt_fact_binding =
    1.32    Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty)
    1.33 -    Attrib.empty_binding;
    1.34 +    Binding.empty_atts;
    1.35  
    1.36  val for_params =
    1.37    Scan.optional