src/HOL/thy_syntax.ML
changeset 1430 439e1476a7f8
parent 1316 ce35d42d2190
child 1465 5d7a7e439cec
     1.1 --- a/src/HOL/thy_syntax.ML	Mon Jan 01 11:54:36 1996 +0100
     1.2 +++ b/src/HOL/thy_syntax.ML	Tue Jan 02 10:46:50 1996 +0100
     1.3 @@ -51,30 +51,34 @@
     1.4        in
     1.5           (";\n\n\
     1.6            \structure " ^ stri_name ^ " =\n\
     1.7 -          \ let open Ind_Syntax in\n\
     1.8            \  struct\n\
     1.9            \  val _ = writeln \"" ^ co ^
    1.10                       "Inductive definition " ^ big_rec_name ^ "\"\n\
    1.11 -          \  val rec_tms\t= map (readtm (sign_of thy) termTVar) "
    1.12 +          \  val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.termTVar) "
    1.13                             ^ srec_tms ^ "\n\
    1.14            \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
    1.15                             ^ sintrs ^ "\n\
    1.16 -          \  end\n\
    1.17 -          \ end;\n\n\
    1.18 +          \  end;\n\n\
    1.19            \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^
    1.20               stri_name ^ ".rec_tms, " ^
    1.21               stri_name ^ ".intr_tms)"
    1.22           ,
    1.23            "structure " ^ big_rec_name ^ " =\n\
    1.24 -          \  struct\n\
    1.25 +          \ let\n\
    1.26 +          \  val _ = writeln \"Proofs for " ^ co ^ 
    1.27 +                     "Inductive definition " ^ big_rec_name ^ "\"\n\
    1.28            \  structure Result = " ^ co ^ "Ind_section_Fun\n\
    1.29 -          \  (open " ^ stri_name ^ "\n\
    1.30 -          \   val thy\t\t= thy\n\
    1.31 -          \   val monos\t\t= " ^ monos ^ "\n\
    1.32 -          \   val con_defs\t\t= " ^ con_defs ^ ");\n\n\
    1.33 +          \\t  (open " ^ stri_name ^ "\n\
    1.34 +          \\t   val thy\t\t= thy\n\
    1.35 +          \\t   val monos\t\t= " ^ monos ^ "\n\
    1.36 +          \\t   val con_defs\t\t= " ^ con_defs ^ ");\n\n\
    1.37 +	  \ in\n\
    1.38 +          \  struct\n\
    1.39            \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
    1.40            \  open Result\n\
    1.41 -          \  end\n"
    1.42 +          \  end\n\
    1.43 +          \ end;\n\n\
    1.44 +          \structure " ^ stri_name ^ " = struct end;\n\n"
    1.45           )
    1.46        end
    1.47      val ipairs = "intrs" $$-- repeat1 (ident -- !! string)