# HG changeset patch
# User haftmann
# Date 1178785304 -7200
# Node ID 8caf6da610e29d3ce51a3607f92f514ffe1a6a43
# Parent  bb8a928a6bfa7451c2c7bda9757627fa375c9b77
tuned

diff -r bb8a928a6bfa -r 8caf6da610e2 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Thu May 10 04:06:56 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Thu May 10 10:21:44 2007 +0200
@@ -81,7 +81,7 @@
     by Stefan Berghofer \cite{Berghofer-Nipkow:2002}.
     So, for the moment, there are two distinct code generators
     in Isabelle.
-    Also note that while the framework itself is largely
+    Also note that while the framework itself is
     object-logic independent, only @{text HOL} provides a reasonable
     framework setup.    
   \end{warn}
@@ -91,7 +91,8 @@
 section {* An example: a simple theory of search trees \label{sec:example} *}
 
 text {*
-  When writing executable specifications, it is convenient to use
+  When writing executable specifications using @{text HOL},
+  it is convenient to use
   three existing packages: the datatype package for defining
   datatypes, the function package for (recursive) functions,
   and the class package for overloaded definitions.
@@ -208,7 +209,7 @@
 subsection {* Invoking the code generator *}
 
 text {*
-  Thanks to a reasonable setup of the HOL theories, in
+  Thanks to a reasonable setup of the @{text HOL} theories, in
   most cases code generation proceeds without further ado:
 *}
 
@@ -277,7 +278,7 @@
   defining equations (the additional stuff displayed
   shall not bother us for the moment).
 
-  The typical HOL tools are already set up in a way that
+  The typical @{text HOL} tools are already set up in a way that
   function definitions introduced by @{text "\<DEFINITION>"},
   @{text "\<FUN>"},
   @{text "\<FUNCTION>"}, @{text "\<PRIMREC>"},
@@ -450,17 +451,18 @@
 subsection {* Library theories \label{sec:library} *}
 
 text {*
-  The HOL \emph{Main} theory already provides a code generator setup
+  The @{text HOL} @{text Main} theory already provides a code
+  generator setup
   which should be suitable for most applications. Common extensions
-  and modifications are available by certain theories of the HOL
+  and modifications are available by certain theories of the @{text HOL}
   library; beside being useful in applications, they may serve
   as a tutorial for customizing the code generator setup.
 
   \begin{description}
 
-    \item[@{text "Pretty_Int"}] represents HOL integers by big
+    \item[@{text "Pretty_Int"}] represents @{text HOL} integers by big
        integer literals in target languages.
-    \item[@{text "Pretty_Char"}] represents HOL characters by 
+    \item[@{text "Pretty_Char"}] represents @{text HOL} characters by 
        character literals in target languages.
     \item[@{text "Pretty_Char_chr"}] like @{text "Pretty_Char_chr"},
        but also offers treatment of character codes; includes
@@ -474,11 +476,18 @@
        matching with @{const "0\<Colon>nat"} / @{const "Suc"}
        is eliminated;  includes @{text "Pretty_Int"}.
     \item[@{text "MLString"}] provides an additional datatype @{text "mlstring"};
-       in the HOL default setup, strings in HOL are mapped to list
-       of HOL characters in SML; values of type @{text "mlstring"} are
+       in the @{text HOL} default setup, strings in HOL are mapped to list
+       of @{text HOL} characters in SML; values of type @{text "mlstring"} are
        mapped to strings in SML.
 
   \end{description}
+
+  \begin{warn}
+    When importing any of these theories, they should form the last
+    items in an import list.  Since these theories adapt the
+    code generator setup in a non-conservative fashion,
+    strange effects may occur otherwise.
+  \end{warn}
 *}
 
 subsection {* Preprocessing *}
diff -r bb8a928a6bfa -r 8caf6da610e2 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu May 10 04:06:56 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu May 10 10:21:44 2007 +0200
@@ -106,7 +106,7 @@
     by Stefan Berghofer \cite{Berghofer-Nipkow:2002}.
     So, for the moment, there are two distinct code generators
     in Isabelle.
-    Also note that while the framework itself is largely
+    Also note that while the framework itself is
     object-logic independent, only \isa{HOL} provides a reasonable
     framework setup.    
   \end{warn}%
@@ -118,7 +118,8 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-When writing executable specifications, it is convenient to use
+When writing executable specifications using \isa{HOL},
+  it is convenient to use
   three existing packages: the datatype package for defining
   datatypes, the function package for (recursive) functions,
   and the class package for overloaded definitions.
@@ -241,7 +242,7 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Thanks to a reasonable setup of the HOL theories, in
+Thanks to a reasonable setup of the \isa{HOL} theories, in
   most cases code generation proceeds without further ado:%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -330,7 +331,7 @@
   defining equations (the additional stuff displayed
   shall not bother us for the moment).
 
-  The typical HOL tools are already set up in a way that
+  The typical \isa{HOL} tools are already set up in a way that
   function definitions introduced by \isa{{\isasymDEFINITION}},
   \isa{{\isasymFUN}},
   \isa{{\isasymFUNCTION}}, \isa{{\isasymPRIMREC}},
@@ -571,17 +572,18 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-The HOL \emph{Main} theory already provides a code generator setup
+The \isa{HOL} \isa{Main} theory already provides a code
+  generator setup
   which should be suitable for most applications. Common extensions
-  and modifications are available by certain theories of the HOL
+  and modifications are available by certain theories of the \isa{HOL}
   library; beside being useful in applications, they may serve
   as a tutorial for customizing the code generator setup.
 
   \begin{description}
 
-    \item[\isa{Pretty{\isacharunderscore}Int}] represents HOL integers by big
+    \item[\isa{Pretty{\isacharunderscore}Int}] represents \isa{HOL} integers by big
        integer literals in target languages.
-    \item[\isa{Pretty{\isacharunderscore}Char}] represents HOL characters by 
+    \item[\isa{Pretty{\isacharunderscore}Char}] represents \isa{HOL} characters by 
        character literals in target languages.
     \item[\isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr},
        but also offers treatment of character codes; includes
@@ -595,11 +597,18 @@
        matching with \isa{{\isadigit{0}}} / \isa{Suc}
        is eliminated;  includes \isa{Pretty{\isacharunderscore}Int}.
     \item[\isa{MLString}] provides an additional datatype \isa{mlstring};
-       in the HOL default setup, strings in HOL are mapped to list
-       of HOL characters in SML; values of type \isa{mlstring} are
+       in the \isa{HOL} default setup, strings in HOL are mapped to list
+       of \isa{HOL} characters in SML; values of type \isa{mlstring} are
        mapped to strings in SML.
 
-  \end{description}%
+  \end{description}
+
+  \begin{warn}
+    When importing any of these theories, they should form the last
+    items in an import list.  Since these theories adapt the
+    code generator setup in a non-conservative fashion,
+    strange effects may occur otherwise.
+  \end{warn}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r bb8a928a6bfa -r 8caf6da610e2 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu May 10 04:06:56 2007 +0200
+++ b/src/HOL/Divides.thy	Thu May 10 10:21:44 2007 +0200
@@ -34,7 +34,7 @@
 instance nat :: "Divides.div"
   mod_def: "m mod n == wfrec (pred_nat^+)
                           (%f j. if j<n | n=0 then j else f (j-n)) m"
-  div_def:   "m div n == wfrec (pred_nat^+)
+  div_def: "m div n == wfrec (pred_nat^+)
                           (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" ..
 
 definition
diff -r bb8a928a6bfa -r 8caf6da610e2 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Thu May 10 04:06:56 2007 +0200
+++ b/src/HOL/Lattices.thy	Thu May 10 10:21:44 2007 +0200
@@ -13,8 +13,8 @@
 
 text{*
   This theory of lattices only defines binary sup and inf
-  operations. The extension to (finite) sets is done in theories
-  @{text FixedPoint} and @{text Finite_Set}.
+  operations. The extension to complete lattices is done in theory
+  @{text FixedPoint}.
 *}
 
 class lower_semilattice = order +
@@ -278,17 +278,24 @@
 qed
   
 
-subsection {* min/max on linear orders as special case of inf/sup *}
+subsection {* @{const min}/@{const max} on linear orders as
+  special case of @{const inf}/@{const sup} *}
+
+lemma (in linorder) distrib_lattice_min_max:
+  "distrib_lattice_pred (op \<^loc>\<le>) (op \<^loc><) min max"
+proof unfold_locales
+  have aux: "\<And>x y \<Colon> 'a. x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> x \<Longrightarrow> x = y"
+    by (auto simp add: less_le antisym)
+  fix x y z
+  show "max x (min y z) = min (max x y) (max x z)"
+  unfolding min_def max_def
+    by (auto simp add: intro: antisym, unfold not_le,
+      auto intro: less_trans le_less_trans aux)
+qed (auto simp add: min_def max_def not_le less_imp_le)
 
 interpretation min_max:
   distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
-apply unfold_locales
-apply (simp add: min_def linorder_not_le order_less_imp_le)
-apply (simp add: min_def linorder_not_le order_less_imp_le)
-apply (simp add: min_def linorder_not_le order_less_imp_le)
-apply (simp add: max_def linorder_not_le order_less_imp_le)
-apply (simp add: max_def linorder_not_le order_less_imp_le)
-unfolding min_def max_def by auto
+  by (rule distrib_lattice_min_max [unfolded linorder_class_min linorder_class_max])
 
 lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   by (rule ext)+ auto
diff -r bb8a928a6bfa -r 8caf6da610e2 src/HOL/Library/AssocList.thy
--- a/src/HOL/Library/AssocList.thy	Thu May 10 04:06:56 2007 +0200
+++ b/src/HOL/Library/AssocList.thy	Thu May 10 10:21:44 2007 +0200
@@ -7,7 +7,6 @@
 
 theory AssocList 
 imports Map
-
 begin
 
 text {*
@@ -541,32 +540,20 @@
 subsection {* @{const compose} *}
 (* ******************************************************************************** *)
 
-lemma compose_induct [case_names Nil Cons]: 
-  fixes xs ys
-  assumes Nil: "P [] ys"
-  assumes Cons: "\<And>x xs.
-     (\<And>v. map_of ys (snd x) = Some v \<Longrightarrow> P xs ys)
-     \<Longrightarrow> (map_of ys (snd x) = None \<Longrightarrow> P (delete (fst x) xs) ys)
-     \<Longrightarrow> P (x # xs) ys"
-  shows "P xs ys"
-by (induct xs rule: compose.induct [where ?P="\<lambda>xs zs. P xs ys"])
-  (auto intro: Nil Cons)
 lemma compose_first_None [simp]: 
   assumes "map_of xs k = None" 
   shows "map_of (compose xs ys) k = None"
-using prems
-by (induct xs ys rule: compose_induct) (auto split: option.splits split_if_asm)
+using prems by (induct xs ys rule: compose.induct)
+  (auto split: option.splits split_if_asm)
 
 lemma compose_conv: 
   shows "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
-proof (induct xs ys rule: compose_induct)
-  case Nil thus ?case by simp
+proof (induct xs ys rule: compose.induct)
+  case 1 then show ?case by simp
 next
-  case (Cons x xs)
-  show ?case
+  case (2 x xs ys) show ?case
   proof (cases "map_of ys (snd x)")
-    case None
-    with Cons
+    case None with 2
     have hyp: "map_of (compose (delete (fst x) xs) ys) k =
                (map_of ys \<circ>\<^sub>m map_of (delete (fst x) xs)) k"
       by simp
@@ -589,7 +576,7 @@
     qed
   next
     case (Some v)
-    with Cons
+    with 2
     have "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
       by simp
     with Some show ?thesis
@@ -607,14 +594,14 @@
 using prems by (simp add: compose_conv)
 
 lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
-proof (induct xs ys rule: compose_induct)
-  case Nil thus ?case by simp
+proof (induct xs ys rule: compose.induct)
+  case 1 thus ?case by simp
 next
-  case (Cons x xs)
+  case (2 x xs ys)
   show ?case
   proof (cases "map_of ys (snd x)")
     case None
-    with Cons.hyps
+    with "2.hyps"
     have "fst ` set (compose (delete (fst x) xs) ys) \<subseteq> fst ` set (delete (fst x) xs)"
       by simp
     also
@@ -625,7 +612,7 @@
       by auto
   next
     case (Some v)
-    with Cons.hyps
+    with "2.hyps"
     have "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
       by simp
     with Some show ?thesis
@@ -637,30 +624,30 @@
  assumes "distinct (map fst xs)"
  shows "distinct (map fst (compose xs ys))"
 using prems
-proof (induct xs ys rule: compose_induct)
-  case Nil thus ?case by simp
+proof (induct xs ys rule: compose.induct)
+  case 1 thus ?case by simp
 next
-  case (Cons x xs)
+  case (2 x xs ys)
   show ?case
   proof (cases "map_of ys (snd x)")
     case None
-    with Cons show ?thesis by simp
+    with 2 show ?thesis by simp
   next
     case (Some v)
-    with Cons dom_compose [of xs ys] show ?thesis 
+    with 2 dom_compose [of xs ys] show ?thesis 
       by (auto)
   qed
 qed
 
 lemma compose_delete_twist: "(compose (delete k xs) ys) = delete k (compose xs ys)"
-proof (induct xs ys rule: compose_induct)
-  case Nil thus ?case by simp
+proof (induct xs ys rule: compose.induct)
+  case 1 thus ?case by simp
 next
-  case (Cons x xs)
+  case (2 x xs ys)
   show ?case
   proof (cases "map_of ys (snd x)")
     case None
-    with Cons have 
+    with 2 have 
       hyp: "compose (delete k (delete (fst x) xs)) ys =
             delete k (compose (delete (fst x) xs) ys)"
       by simp
@@ -678,14 +665,14 @@
     qed
   next
     case (Some v)
-    with Cons have hyp: "compose (delete k xs) ys = delete k (compose xs ys)" by simp
+    with 2 have hyp: "compose (delete k xs) ys = delete k (compose xs ys)" by simp
     with Some show ?thesis
       by simp
   qed
 qed
 
 lemma compose_clearjunk: "compose xs (clearjunk ys) = compose xs ys"
-  by (induct xs ys rule: compose_induct) 
+  by (induct xs ys rule: compose.induct) 
      (auto simp add: map_of_clearjunk split: option.splits)
    
 lemma clearjunk_compose: "clearjunk (compose xs ys) = compose (clearjunk xs) ys"
@@ -695,8 +682,7 @@
    
 lemma compose_empty [simp]:
  "compose xs [] = []"
-  by (induct xs rule: compose_induct [where ys="[]"]) auto
-
+  by (induct xs) (auto simp add: compose_delete_twist)
 
 lemma compose_Some_iff:
   "(map_of (compose xs ys) k = Some v) = 
diff -r bb8a928a6bfa -r 8caf6da610e2 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu May 10 04:06:56 2007 +0200
+++ b/src/HOL/Orderings.thy	Thu May 10 10:21:44 2007 +0200
@@ -81,6 +81,8 @@
 notation (input)
   greater_eq  (infix "\<ge>" 50)
 
+hide const min max
+
 definition
   min :: "'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> 'a" where
   "min a b = (if a \<le> b then a else b)"
@@ -89,11 +91,11 @@
   max :: "'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> 'a" where
   "max a b = (if a \<le> b then b else a)"
 
-lemma min_linorder:
+lemma linorder_class_min:
   "ord.min (op \<le> \<Colon> 'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> bool) = min"
   by rule+ (simp add: min_def ord_class.min_def)
 
-lemma max_linorder:
+lemma linorder_class_max:
   "ord.max (op \<le> \<Colon> 'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> bool) = max"
   by rule+ (simp add: max_def ord_class.max_def)
 
@@ -193,6 +195,14 @@
 lemma less_asym': "a \<^loc>< b \<Longrightarrow> b \<^loc>< a \<Longrightarrow> P"
   by (rule less_asym)
 
+
+text {* Reverse order *}
+
+lemma order_reverse:
+  "order_pred (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
+  by unfold_locales
+    (simp add: less_le, auto intro: antisym order_trans)
+
 end
 
 
@@ -252,6 +262,15 @@
 lemma not_leE: "\<not> y \<^loc>\<le> x \<Longrightarrow> x \<^loc>< y"
   unfolding not_le .
 
+
+text {* Reverse order *}
+
+lemma linorder_reverse:
+  "linorder_pred (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
+  by unfold_locales
+    (simp add: less_le, auto intro: antisym order_trans simp add: linear)
+
+
 text {* min/max properties *}
 
 lemma min_le_iff_disj:
@@ -288,8 +307,7 @@
 
 end
 
-
-subsection {* Name duplicates *}
+subsection {* Name duplicates -- including min/max interpretation *}
 
 lemmas order_less_le = less_le
 lemmas order_eq_refl = order_class.eq_refl
@@ -330,6 +348,15 @@
 lemmas leD = linorder_class.leD
 lemmas not_leE = linorder_class.not_leE
 
+lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [unfolded linorder_class_min]
+lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [unfolded linorder_class_max]
+lemmas min_less_iff_disj = linorder_class.min_less_iff_disj [unfolded linorder_class_min]
+lemmas less_max_iff_disj = linorder_class.less_max_iff_disj [unfolded linorder_class_max]
+lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj [unfolded linorder_class_min]
+lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj [unfolded linorder_class_max]
+lemmas split_min = linorder_class.split_min [unfolded linorder_class_min]
+lemmas split_max = linorder_class.split_max [unfolded linorder_class_max]
+
 
 subsection {* Reasoning tools setup *}
 
@@ -346,18 +373,18 @@
         T <> HOLogic.natT andalso T <> HOLogic.intT
           andalso T <> HOLogic.realT andalso Sign.of_sort thy (T, sort)
       end;
-    fun dec (Const ("Not", _) $ t) = (case dec t
+    fun dec (Const (@{const_name Not}, _) $ t) = (case dec t
           of NONE => NONE
            | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
-      | dec (Const ("op =",  _) $ t1 $ t2) =
+      | dec (Const (@{const_name "op ="},  _) $ t1 $ t2) =
           if of_sort t1
           then SOME (t1, "=", t2)
           else NONE
-      | dec (Const ("Orderings.less_eq",  _) $ t1 $ t2) =
+      | dec (Const (@{const_name less_eq},  _) $ t1 $ t2) =
           if of_sort t1
           then SOME (t1, "<=", t2)
           else NONE
-      | dec (Const ("Orderings.less",  _) $ t1 $ t2) =
+      | dec (Const (@{const_name less},  _) $ t1 $ t2) =
           if of_sort t1
           then SOME (t1, "<", t2)
           else NONE
@@ -417,7 +444,7 @@
 
 fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
   let val prems = prems_of_ss ss;
-      val less = Const("Orderings.less",T);
+      val less = Const (@{const_name less}, T);
       val t = HOLogic.mk_Trueprop(le $ s $ r);
   in case find_first (prp t) prems of
        NONE =>
@@ -432,7 +459,7 @@
 
 fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) =
   let val prems = prems_of_ss ss;
-      val le = Const("Orderings.less_eq",T);
+      val le = Const (@{const_name less_eq}, T);
       val t = HOLogic.mk_Trueprop(le $ r $ s);
   in case find_first (prp t) prems of
        NONE =>
@@ -521,12 +548,12 @@
 
 print_translation {*
 let
-  val All_binder = Syntax.binder_name @{const_syntax "All"};
-  val Ex_binder = Syntax.binder_name @{const_syntax "Ex"};
+  val All_binder = Syntax.binder_name @{const_syntax All};
+  val Ex_binder = Syntax.binder_name @{const_syntax Ex};
   val impl = @{const_syntax "op -->"};
   val conj = @{const_syntax "op &"};
-  val less = @{const_syntax "less"};
-  val less_eq = @{const_syntax "less_eq"};
+  val less = @{const_syntax less};
+  val less_eq = @{const_syntax less_eq};
 
   val trans =
    [((All_binder, impl, less), ("_All_less", "_All_greater")),
@@ -801,7 +828,7 @@
 instance bool :: order 
   le_bool_def: "P \<le> Q \<equiv> P \<longrightarrow> Q"
   less_bool_def: "P < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
-  by default (auto simp add: le_bool_def less_bool_def)
+  by intro_classes (auto simp add: le_bool_def less_bool_def)
 
 lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
   by (simp add: le_bool_def)
@@ -854,15 +881,6 @@
   apply (auto intro!: order_antisym)
   done
 
-lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [unfolded min_linorder]
-lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [unfolded max_linorder]
-lemmas min_less_iff_disj = linorder_class.min_less_iff_disj [unfolded min_linorder]
-lemmas less_max_iff_disj = linorder_class.less_max_iff_disj [unfolded max_linorder]
-lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj [unfolded min_linorder]
-lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj [unfolded max_linorder]
-lemmas split_min = linorder_class.split_min [unfolded min_linorder]
-lemmas split_max = linorder_class.split_max [unfolded max_linorder]
-
 lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
   by (simp add: min_def)
 
diff -r bb8a928a6bfa -r 8caf6da610e2 src/Pure/Tools/codegen_func.ML
--- a/src/Pure/Tools/codegen_func.ML	Thu May 10 04:06:56 2007 +0200
+++ b/src/Pure/Tools/codegen_func.ML	Thu May 10 10:21:44 2007 +0200
@@ -103,7 +103,7 @@
       | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
       | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty
           then bad_thm
-            ("Partially applied constant on left hand side of equation"
+            ("Partially applied constant on left hand side of equation\n"
                ^ Display.string_of_thm thm)
           else ();
     val _ = map (check 0) args;