equal
deleted
inserted
replaced
421 |
421 |
422 val instanceP = |
422 val instanceP = |
423 OuterSyntax.command instanceK "" K.thy_goal |
423 OuterSyntax.command instanceK "" K.thy_goal |
424 (P.xname -- (P.$$$ "::" |-- P.!!! P.arity) |
424 (P.xname -- (P.$$$ "::" |-- P.!!! P.arity) |
425 -- Scan.repeat1 P.spec_name |
425 -- Scan.repeat1 P.spec_name |
426 >> (Toplevel.theory_theory_to_proof |
426 >> (Toplevel.theory_to_proof |
427 o (fn ((tyco, (asorts, sort)), defs) => add_instance_arity ((tyco, asorts), sort) defs))); |
427 o (fn ((tyco, (asorts, sort)), defs) => add_instance_arity ((tyco, asorts), sort) defs))); |
428 |
428 |
429 val _ = OuterSyntax.add_parsers [classP, instanceP]; |
429 val _ = OuterSyntax.add_parsers [classP, instanceP]; |
430 |
430 |
431 end; (* local *) |
431 end; (* local *) |