src/Pure/Isar/attrib.ML
changeset 35625 9c818cab0dd0
parent 35624 c4e29a0bb8c1
child 35979 12bb31230550
     1.1 --- a/src/Pure/Isar/attrib.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -252,7 +252,7 @@
     1.4  (* rule format *)
     1.5  
     1.6  val rule_format = Args.mode "no_asm"
     1.7 -  >> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format);
     1.8 +  >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format);
     1.9  
    1.10  val elim_format = Thm.rule_attribute (K Tactic.make_elim);
    1.11  
    1.12 @@ -306,9 +306,9 @@
    1.13    setup (Binding.name "no_vars") (Scan.succeed no_vars) "frozen schematic vars" #>
    1.14    setup (Binding.name "eta_long") (Scan.succeed eta_long)
    1.15      "put theorem into eta long beta normal form" #>
    1.16 -  setup (Binding.name "atomize") (Scan.succeed ObjectLogic.declare_atomize)
    1.17 +  setup (Binding.name "atomize") (Scan.succeed Object_Logic.declare_atomize)
    1.18      "declaration of atomize rule" #>
    1.19 -  setup (Binding.name "rulify") (Scan.succeed ObjectLogic.declare_rulify)
    1.20 +  setup (Binding.name "rulify") (Scan.succeed Object_Logic.declare_rulify)
    1.21      "declaration of rulify rule" #>
    1.22    setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #>
    1.23    setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del)