--- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Mar 16 14:46:13 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Mar 16 18:20:12 2012 +0100
@@ -264,17 +264,15 @@
val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false
-val quotspec_parser =
- Parse.and_list1
- ((Parse.type_args -- Parse.binding) --
- (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
- Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
- (@{keyword "/"} |-- (partial -- Parse.term)) --
- Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
-
val _ =
- Outer_Syntax.local_theory_to_proof "quotient_type"
+ Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
"quotient type definitions (require equivalence proofs)"
- Keyword.thy_goal (quotspec_parser >> quotient_type_cmd)
+ (Parse.and_list1
+ ((Parse.type_args -- Parse.binding) --
+ (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
+ Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
+ (@{keyword "/"} |-- (partial -- Parse.term)) --
+ Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
+ >> quotient_type_cmd)
end;