diff -r 5023b3d34e15 -r b89aed3c5437 Inductive.ML
--- a/Inductive.ML	Fri Nov 04 14:16:39 1994 +0100
+++ b/Inductive.ML	Fri Nov 04 14:17:20 1994 +0100
@@ -92,50 +92,3 @@
 
 
 structure CoInd = Add_inductive_def_Fun(Gfp_items);
-
-
-
-(*For installing the theory section.   co is either "" or "Co"*)
-fun inductive_decl co =
-  let open ThyParse Ind_Syntax
-      fun mk_intr_name (s,_) =  (*the "op" cancels any infix status*)
-	  if Syntax.is_identifier s then "op " ^ s  else "_"
-      fun mk_params (((recs, ipairs), monos), con_defs) =
-        let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs)
-	    and srec_tms = mk_list recs
-            and sintrs   = mk_big_list (map snd ipairs)
-            val stri_name = big_rec_name ^ "_Intrnl"
-        in
-	   (";\n\n\
-            \structure " ^ stri_name ^ " =\n\
-            \ let open Ind_Syntax in\n\
-            \  struct\n\
-            \  val _ = writeln \"" ^ co ^ 
-	               "Inductive definition " ^ big_rec_name ^ "\"\n\
-            \  val rec_tms\t= map (readtm (sign_of thy) termTVar) "
-	                     ^ srec_tms ^ "\n\
-            \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
-	                     ^ sintrs ^ "\n\
-            \  end\n\
-            \ end;\n\n\
-            \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^ 
-	       stri_name ^ ".rec_tms, " ^
-               stri_name ^ ".intr_tms)"
-           ,
-	    "structure " ^ big_rec_name ^ " =\n\
-            \  struct\n\
-            \  structure Result = " ^ co ^ "Ind_section_Fun\n\
-            \  (open " ^ stri_name ^ "\n\
-            \   val thy\t\t= thy\n\
-            \   val monos\t\t= " ^ monos ^ "\n\
-            \   val con_defs\t\t= " ^ con_defs ^ ");\n\n\
-            \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
-            \  open Result\n\
-            \  end\n"
-	   )
-	end
-      val ipairs  = "intrs"   $$-- repeat1 (ident -- !! string)
-      fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
-  in repeat1 string -- ipairs -- optstring "monos" -- optstring "con_defs"
-     >> mk_params
-  end;