src/Pure/Isar/isar_syn.ML
changeset 22796 34c316d7b630
parent 22744 5cbe966d67a2
child 22866 9de680b7d819
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Apr 26 12:00:01 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Apr 26 12:00:05 2007 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4  
     1.5  val defaultsortP =
     1.6    OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
     1.7 -    (P.sort >> (Toplevel.theory o Theory.add_defsort));
     1.8 +    (P.sort >> (Toplevel.theory o Sign.add_defsort));
     1.9  
    1.10  val axclassP =
    1.11    OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
    1.12 @@ -97,18 +97,18 @@
    1.13  val typedeclP =
    1.14    OuterSyntax.command "typedecl" "type declaration" K.thy_decl
    1.15      (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) =>
    1.16 -      Toplevel.theory (Theory.add_typedecls [(a, args, mx)])));
    1.17 +      Toplevel.theory (Sign.add_typedecls [(a, args, mx)])));
    1.18  
    1.19  val typeabbrP =
    1.20    OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
    1.21      (Scan.repeat1
    1.22        (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')))
    1.23 -      >> (Toplevel.theory o Theory.add_tyabbrs o
    1.24 +      >> (Toplevel.theory o Sign.add_tyabbrs o
    1.25          map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
    1.26  
    1.27  val nontermP =
    1.28    OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
    1.29 -    K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Theory.add_nonterminals));
    1.30 +    K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Sign.add_nonterminals));
    1.31  
    1.32  val aritiesP =
    1.33    OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
    1.34 @@ -123,7 +123,7 @@
    1.35  
    1.36  val constsP =
    1.37    OuterSyntax.command "consts" "declare constants" K.thy_decl
    1.38 -    (Scan.repeat1 P.const >> (Toplevel.theory o Theory.add_consts));
    1.39 +    (Scan.repeat1 P.const >> (Toplevel.theory o Sign.add_consts));
    1.40  
    1.41  val opt_overloaded = P.opt_keyword "overloaded";
    1.42  
    1.43 @@ -139,11 +139,11 @@
    1.44  
    1.45  val syntaxP =
    1.46    OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
    1.47 -    (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.add_modesyntax));
    1.48 +    (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.add_modesyntax));
    1.49  
    1.50  val no_syntaxP =
    1.51    OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl
    1.52 -    (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.del_modesyntax));
    1.53 +    (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.del_modesyntax));
    1.54  
    1.55  
    1.56  (* translations *)
    1.57 @@ -162,11 +162,11 @@
    1.58  
    1.59  val translationsP =
    1.60    OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl
    1.61 -    (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules));
    1.62 +    (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.add_trrules));
    1.63  
    1.64  val no_translationsP =
    1.65    OuterSyntax.command "no_translations" "remove syntax translation rules" K.thy_decl
    1.66 -    (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.del_trrules));
    1.67 +    (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.del_trrules));
    1.68  
    1.69  
    1.70  (* axioms and definitions *)