--- a/src/Pure/Isar/isar_syn.ML Wed Jan 21 16:47:02 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML Wed Jan 21 16:47:03 2009 +0100
@@ -418,45 +418,6 @@
>> (fn expr => Toplevel.print o
Toplevel.proof' (fn int => Expression.interpret_cmd expr int)));
-local
-
-val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Binding.empty;
-
-in
-
-val locale_val =
- SpecParse.locale_expr --
- Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
- Scan.repeat1 SpecParse.context_element >> pair Old_Locale.empty;
-
-val _ =
- OuterSyntax.command "class_locale" "define named proof context based on classes" K.thy_decl
- (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Old_Locale.empty, []) -- P.opt_begin
- >> (fn ((name, (expr, elems)), begin) =>
- (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
- (Old_Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin)));
-
-val _ =
- OuterSyntax.command "class_interpretation"
- "prove and register interpretation of locale expression in theory or locale" K.thy_goal
- (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
- >> (Toplevel.print oo (Toplevel.theory_to_proof o Old_Locale.interpretation_in_locale I)) ||
- opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
- >> (fn ((name, expr), insts) => Toplevel.print o
- Toplevel.theory_to_proof
- (Old_Locale.interpretation_cmd (Binding.base_name name) expr insts)));
-
-val _ =
- OuterSyntax.command "class_interpret"
- "prove and register interpretation of locale expression in proof context"
- (K.tag_proof K.prf_goal)
- (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
- >> (fn ((name, expr), insts) => Toplevel.print o
- Toplevel.proof'
- (fn int => Old_Locale.interpret_cmd (Binding.base_name name) expr insts int)));
-
-end;
-
(* classes *)
@@ -857,12 +818,6 @@
(opt_bang -- P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
val _ =
- OuterSyntax.improper_command "print_interps"
- "print interpretations of named locale" K.diag
- (Scan.optional (P.$$$ "!" >> K true) false -- P.xname
- >> (Toplevel.no_timing oo uncurry IsarCmd.print_registrations));
-
-val _ =
OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));