--- a/src/HOL/BNF/Tools/bnf_fp.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML Wed Sep 26 10:00:59 2012 +0200
@@ -7,6 +7,10 @@
signature BNF_FP =
sig
+ type fp_result =
+ BNF_Def.BNF list * term list * term list * term list * term list * thm * thm * thm list *
+ thm list * thm list * thm list * thm list list * thm list * thm list * thm list
+
val time: Timer.real_timer -> string -> Timer.real_timer
val IITN: string
@@ -91,7 +95,7 @@
val simpsN: string
val strTN: string
val str_initN: string
- val strongN: string
+ val strong_coinductN: string
val sum_bdN: string
val sum_bdTN: string
val unfoldN: string
@@ -160,6 +164,10 @@
open BNF_Def
open BNF_Util
+type fp_result =
+ BNF_Def.BNF list * term list * term list * term list * term list * thm * thm * thm list *
+ thm list * thm list * thm list * thm list list * thm list * thm list * thm list;
+
val timing = true;
fun time timer msg = (if timing
then warning (msg ^ ": " ^ ATP_Util.string_from_time (Timer.checkRealTimer timer))
@@ -242,10 +250,10 @@
val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN
val dtor_coinductN = dtorN ^ "_" ^ coinductN
val dtor_srel_coinductN = dtor_srelN ^ "_" ^ coinductN
-val strongN = "strong_"
-val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strongN ^ coinductN
-val dtor_strong_coinductN = dtorN ^ "_" ^ strongN ^ coinductN
-val dtor_srel_strong_coinductN = dtor_srelN ^ "_" ^ strongN ^ coinductN
+val strong_coinductN = "strong_" ^ coinductN
+val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strong_coinductN
+val dtor_strong_coinductN = dtorN ^ "_" ^ strong_coinductN
+val dtor_srel_strong_coinductN = dtor_srelN ^ "_" ^ strong_coinductN
val hsetN = "Hset"
val hset_recN = hsetN ^ "_rec"
val set_inclN = "set_incl"
@@ -408,7 +416,7 @@
val Ds = fold (fold Term.add_tfreesT) deadss [];
val _ = (case Library.inter (op =) Ds lhss of [] => ()
- | A :: _ => error ("Nonadmissible type recursion (cannot take fixed point of dead type \
+ | A :: _ => error ("Inadmissible type recursion (cannot take fixed point of dead type \
\variable " ^ quote (Syntax.string_of_typ lthy (TFree A)) ^ ")"));
val timer = time (timer "Construction of BNFs");