diff -r c843e5a4e0a4 -r 3b1e8c22a44e datatype.ML
--- a/datatype.ML	Wed Nov 23 10:41:42 1994 +0100
+++ b/datatype.ML	Wed Nov 23 15:09:44 1994 +0100
@@ -1,108 +1,10 @@
-(* Title:  HOL/Datatype
-   ID:     $Id$
-   Author: Max Breitling, Carsten Clasohm,
-           Tobias Nipkow, Norbert Voelker
+(* Title:       HOL/datatype.ML
+   ID:          $Id$
+   Author:      Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker
    Copyright 1994 TU Muenchen
 *)
 
 
-(*choice between Ci_neg1 and Ci_neg2 axioms depends on number of constructors*)
-local
-
-  val dtK = 5
-
-in
-
-local open ThyParse in
-  val datatype_decls =
-    let 
-      val tvar = type_var >> (fn s => "dtVar" ^ s);
-    
-      val type_var_list = 
-	tvar >> (fn s => [s]) || "(" $$-- list1 tvar --$$ ")";
-    
-      val typ =
-	ident                  >> (fn s => "dtTyp([]," ^ quote s ^")")
-      ||
-	type_var_list -- ident >> (fn (ts, id) => "dtTyp(" ^ mk_list ts ^
-				   "," ^ quote id ^ ")")
-      ||
-	tvar;
-    
-      val typ_list = "(" $$-- list1 typ --$$ ")" || empty;
-      
-      val cons = name -- typ_list -- opt_mixfix;
-  
-      fun constructs ts =
-	( cons --$$ "|" -- constructs >> op::
-      ||
-	 cons                        >> (fn c => [c])) ts;  
-  
-      fun mk_cons cs =
-	case findrep (map (fst o fst) cs) of
-	  [] => map (fn ((s,ts),syn) => parens(commas [s,mk_list ts,syn])) cs
-	| c::_ => error("Constructor \"" ^ c ^ "\" occurs twice");
-      
-      (*remove all quotes from a string*)
-      val rem_quotes = implode o filter (fn c => c <> "\"") o explode;
-
-      (*generate names of distinct axioms*)
-      fun rules_distinct cs tname = 
-        let val uqcs = map (fn ((s,_),_) => rem_quotes s) cs;
-      (*combine all constructor names with all others w/o duplicates*)
-	  fun negOne c = map (fn c2 => quote (c ^ "_not_" ^ c2));
-	  fun neg1 [] = []
-	    | neg1 (c1 :: cs) = (negOne c1 cs) @ (neg1 cs)
-	in if length uqcs < dtK then neg1 uqcs
-	   else quote (tname ^ "_ord_distinct") ::
-	     map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs
-	end;
-         
-      fun rules tname cons pre =
-	" map (get_axiom thy) " ^
-	mk_list (map (fn ((s,_),_) => quote(tname ^ pre ^ rem_quotes s))
-		   cons)
-
-	(*generate string for calling 'add_datatype'*)
-      fun mk_params ((ts, tname), cons) =
-	("val (thy," ^ tname ^ "_add_primrec) =  add_datatype\n" ^
-	 parens (commas [mk_list ts, quote tname, mk_list (mk_cons cons)]) ^
-	 " thy\n\
-	  \val thy=thy",
-	 "structure " ^ tname ^ " =\n\
-	  \struct\n\
-	  \  val inject = map (get_axiom thy) " ^
-	 mk_list (map (fn ((s,_), _) => quote ("inject_" ^ rem_quotes s)) 
-		  (filter_out (null o snd o fst) cons)) ^ ";\n\
-		   \  val distinct = " ^ 
-	 (if length cons < dtK then "let val distinct' = " else "") ^ 
-	    "map (get_axiom thy) " ^ mk_list (rules_distinct cons tname) ^ 
-	    (if length cons < dtK then 
-	       "  in distinct' @ (map (fn t => sym COMP (t RS contrapos))\
-		\ distinct') end"
-	     else "") ^ ";\n\
-	      \  val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\
-	      \  val cases =" ^ rules tname cons "_case_" ^ ";\n\
-	      \  val recs =" ^ rules tname cons "_rec_" ^ ";\n\
-	      \  val simps = inject @ distinct @ cases @ recs;\n\
-	      \  fun induct_tac a =\
-	      \res_inst_tac[(" ^ quote tname ^ ", a)]induct;\n\
-	      \end;\n")
-    in 
-      (type_var_list || empty) -- ident --$$ "=" -- constructs >> mk_params 
-end
-
-val primrec_decl =
-  let fun mkstrings((fname,tname),axms) =
-        let fun prove (name,eqn) =
-              "val "^name^"= prove_goalw thy [get_def thy "^fname^"] "^eqn^"\n\
-              \  (fn _ => [simp_tac (HOL_ss addsimps " ^ tname^".recs) 1])"
-            val axs = mk_list (map (fn (n,a) => mk_pair(quote n,a)) axms)
-        in ("|> " ^ tname^"_add_primrec " ^ axs, cat_lines(map prove axms))
-        end
-  in name -- long_id -- repeat1 (ident -- string)  >> mkstrings end
-end;
-
 (*used for constructor parameters*)
 datatype dt_type = dtVar of string |
   dtTyp of dt_type list * string |
@@ -111,7 +13,7 @@
 local 
 
 val mysort = sort;
-open ThyParse
+open ThyParse;
 exception Impossible;
 exception RecError of string;
 
@@ -542,4 +444,3 @@
       |> add_axioms rules,add_primrec)
     end
 end
-end;