src/Pure/Isar/attrib.ML
changeset 35624 c4e29a0bb8c1
parent 35021 c839a4c670c6
child 35625 9c818cab0dd0
     1.1 --- a/src/Pure/Isar/attrib.ML	Sat Mar 06 19:17:59 2010 +0000
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sun Mar 07 11:57:16 2010 +0100
     1.3 @@ -245,8 +245,8 @@
     1.4  fun unfolded_syntax rule =
     1.5    thms >> (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths));
     1.6  
     1.7 -val unfolded = unfolded_syntax LocalDefs.unfold;
     1.8 -val folded = unfolded_syntax LocalDefs.fold;
     1.9 +val unfolded = unfolded_syntax Local_Defs.unfold;
    1.10 +val folded = unfolded_syntax Local_Defs.fold;
    1.11  
    1.12  
    1.13  (* rule format *)
    1.14 @@ -311,7 +311,7 @@
    1.15    setup (Binding.name "rulify") (Scan.succeed ObjectLogic.declare_rulify)
    1.16      "declaration of rulify rule" #>
    1.17    setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #>
    1.18 -  setup (Binding.name "defn") (add_del LocalDefs.defn_add LocalDefs.defn_del)
    1.19 +  setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del)
    1.20      "declaration of definitional transformations" #>
    1.21    setup (Binding.name "abs_def") (Scan.succeed (Thm.rule_attribute (K Drule.abs_def)))
    1.22      "abstract over free variables of a definition"));