src/Pure/Isar/isar_syn.ML
changeset 25462 dad0291cb76a
parent 25290 250c7a0205ca
child 25485 33840a854e63
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Nov 23 21:09:34 2007 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Nov 23 21:09:35 2007 +0100
     1.3 @@ -113,7 +113,7 @@
     1.4  val _ =
     1.5    OuterSyntax.command "typedecl" "type declaration" K.thy_decl
     1.6      (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) =>
     1.7 -      Toplevel.theory (Sign.add_typedecls [(a, args, mx)])));
     1.8 +      Toplevel.theory (Typedecl.add (a, args, mx) #> snd)));
     1.9  
    1.10  val _ =
    1.11    OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
    1.12 @@ -448,18 +448,18 @@
    1.13    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
    1.14    ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
    1.15      P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    1.16 -      >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func (* FIXME ? *))))
    1.17 +      >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func)))
    1.18      >> (Toplevel.print oo Toplevel.theory_to_proof));
    1.19  
    1.20  val _ =
    1.21    OuterSyntax.command "instantiation" "prove type arity" K.thy_decl
    1.22 -   (P.and_list1 P.arity -- P.opt_begin
    1.23 -     >> (fn (arities, begin) => (begin ? Toplevel.print) o
    1.24 -         Toplevel.begin_local_theory begin (Instance.begin_instantiation_cmd arities)));
    1.25 +   (P.and_list1 P.arity --| P.begin
    1.26 +     >> (fn arities => Toplevel.print o
    1.27 +         Toplevel.begin_local_theory true (Instance.instantiation_cmd arities)));
    1.28  
    1.29  val _ =  (* FIXME incorporate into "instance" *)
    1.30    OuterSyntax.command "instance_proof" "prove type arity relation" K.thy_goal
    1.31 -    (Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE Instance.proof_instantiation));
    1.32 +    (Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.proof_instantiation I)));
    1.33  
    1.34  
    1.35  (* code generation *)