diff -r 12448b8f92fb -r 92dbe243555f src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Thu Mar 11 21:57:34 1999 +0100
+++ b/src/HOL/Tools/record_package.ML	Thu Mar 11 21:58:12 1999 +0100
@@ -421,6 +421,8 @@
 
 (** record field splitting **)
 
+(* tactic *)
+
 fun record_split_tac i st =
   let
     val (_, (sps, ss)) = RecordsData.get_sg (Thm.sign_of_thm st);
@@ -433,10 +435,20 @@
     else Seq.empty
   end handle Library.LIST _ => Seq.empty;
 
+
+(* wrapper *)
+
 val record_split_name = "record_split_tac";
 val record_split_wrapper = (record_split_name, fn tac => record_split_tac ORELSE' tac);
 
 
+(* method *)
+
+val record_split_method =
+  ("record_split", Method.no_args (Method.METHOD0 (FIRSTGOAL record_split_tac)),
+    "split record fields");
+
+
 
 (** internal theory extenders **)
 
@@ -858,14 +870,31 @@
 
 
 
-(** setup theory **)
+(** package setup **)
+
+(* setup theory *)
 
 val setup =
  [RecordsData.init,
   Theory.add_trfuns ([], parse_translation, [], []),
+  Method.add_methods [record_split_method],
   add_wrapper record_split_wrapper];
 
 
+(* outer syntax *)
+
+open OuterParse;
+
+val record_decl =
+  type_args -- name -- ($$$ "=" |-- Scan.option (typ --| $$$ "+")
+    -- Scan.repeat1 (name -- ($$$ "::" |-- typ)));
+
+val recordP =
+  OuterSyntax.parser false "record" "define extensible record"
+    (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z)));
+
+val _ = OuterSyntax.add_parsers [recordP];
+
 end;