# HG changeset patch
# User wenzelm
# Date 921185854 -3600
# Node ID 12448b8f92fbc2b25224316bf8a770534ee91915
# Parent  6c01697e082e4c0e6817a29256d1ef3094c16f4d
named witnesses: PureThy.get_thmss;
outer syntax for 'typedecl', 'typedef';

diff -r 6c01697e082e -r 12448b8f92fb src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Thu Mar 11 21:56:22 1999 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Thu Mar 11 21:57:34 1999 +0100
@@ -2,7 +2,10 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Gordon/HOL style type definitions.
+Gordon/HOL-style type definitions.
+
+TODO:
+  - typedefP: elim witness;
 *)
 
 signature TYPEDEF_PACKAGE =
@@ -62,14 +65,12 @@
       if_none usr_tac (TRY (ALLGOALS (CLASET' blast_tac)));
   in
     prove_goalw_cterm [] goal (K [tac])
-  end
-  handle ERROR =>
-    error ("Failed to prove nonemptiness of " ^ quote (string_of_cterm cset));
+  end handle ERROR => error ("Failed to prove nonemptiness of " ^ quote (string_of_cterm cset));
 
 
 (* gen_add_typedef *)
 
-fun gen_add_typedef prep_term no_def name (t, vs, mx) raw_set axms thms usr_tac thy =
+fun gen_add_typedef prep_term no_def name (t, vs, mx) raw_set thm_names thms usr_tac thy =
   let
     val _ = Theory.requires thy "Set" "typedefs";
     val sign = sign_of thy;
@@ -131,7 +132,7 @@
     else error (cat_lines errs);
 
     message ("Proving nonemptiness of " ^ quote name ^ " ...");
-    prove_nonempty cset (map (get_axiom thy) axms @ thms) usr_tac;
+    prove_nonempty cset (PureThy.get_thmss thy thm_names @ thms) usr_tac;
 
     thy
     |> PureThy.add_typedecls [(t, vs, mx)]
@@ -147,9 +148,7 @@
      [(Rep_name, rep_type),
       (Rep_name ^ "_inverse", rep_type_inv),
       (Abs_name ^ "_inverse", abs_type_inv)]
-  end
-  handle ERROR =>
-    error ("The error(s) above occurred in typedef " ^ quote name);
+  end handle ERROR => error ("The error(s) above occurred in typedef " ^ quote name);
 
 
 (* external interfaces *)
@@ -165,4 +164,29 @@
 val add_typedef_i_no_def = gen_add_typedef cert_term true;
 
 
+(* outer syntax *)
+
+open OuterParse;
+
+
+val typedeclP =
+  OuterSyntax.parser false "typedecl" "HOL type declaration"
+    ((type_args -- name -- opt_mixfix) >> (fn ((vs, t), mx) =>
+      Toplevel.theory (add_typedecls [(t, vs, mx)])));
+
+val opt_witness =
+  Scan.optional ($$$ "(" |-- !!! (list1 xname --| $$$ ")")) [];
+
+val typedef_decl =
+  Scan.option ($$$ "(" |-- name --| $$$ ")") --
+    (type_args -- name) -- opt_infix -- ($$$ "=" |-- term -- opt_witness);
+
+val typedefP =
+  OuterSyntax.parser false "typedef" "HOL type definition"
+    (typedef_decl >> (fn (((opt_name, (vs, t)), mx), (A, witn)) =>
+      Toplevel.theory (add_typedef (if_none opt_name t) (t, vs, mx) A witn [] None)));
+
+
+val _ = OuterSyntax.add_parsers [typedeclP, typedefP];
+
 end;