src/Pure/Isar/isar_syn.ML
changeset 25485 33840a854e63
parent 25462 dad0291cb76a
child 25495 98f3596bec44
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Nov 28 09:01:40 2007 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Nov 28 09:01:42 2007 +0100
     1.3 @@ -445,21 +445,20 @@
     1.4        Toplevel.print o Toplevel.local_theory_to_proof loc (Subclass.subclass_cmd class)));
     1.5  
     1.6  val _ =
     1.7 -  OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
     1.8 -  ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
     1.9 -    P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    1.10 -      >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func)))
    1.11 -    >> (Toplevel.print oo Toplevel.theory_to_proof));
    1.12 -
    1.13 -val _ =
    1.14    OuterSyntax.command "instantiation" "prove type arity" K.thy_decl
    1.15     (P.and_list1 P.arity --| P.begin
    1.16       >> (fn arities => Toplevel.print o
    1.17           Toplevel.begin_local_theory true (Instance.instantiation_cmd arities)));
    1.18  
    1.19 -val _ =  (* FIXME incorporate into "instance" *)
    1.20 -  OuterSyntax.command "instance_proof" "prove type arity relation" K.thy_goal
    1.21 -    (Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.proof_instantiation I)));
    1.22 +val _ =
    1.23 +  OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
    1.24 +  ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
    1.25 +    P.$$$ "advanced" |-- P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    1.26 +      >> (fn (arities, defs) => Instance.instance_cmd arities defs (K I)) ||
    1.27 +    P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    1.28 +      >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func)))
    1.29 +    >> (Toplevel.print oo Toplevel.theory_to_proof)
    1.30 +  || Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
    1.31  
    1.32  
    1.33  (* code generation *)