# HG changeset patch
# User wenzelm
# Date 1251476310 -7200
# Node ID 54758ca53fd6f16951032fe1b54d45baa79da01f
# Parent  700ed1f4c576f4ef5bac9968287e73046b8e4835
modernized messages -- eliminated old Display.print_cterm;

diff -r 700ed1f4c576 -r 54758ca53fd6 src/HOL/Nominal/nominal_thmdecls.ML
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Fri Aug 28 17:07:15 2009 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Fri Aug 28 18:18:30 2009 +0200
@@ -74,7 +74,7 @@
     val lhs = Const (@{const_name "perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
     val ([goal_term, pi''], ctxt') = Variable.import_terms false
       [HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt
-    val _ = Display.print_cterm (cterm_of thy goal_term)
+    val _ = writeln (Syntax.string_of_term ctxt' goal_term);
   in
     Goal.prove ctxt' [] [] goal_term
       (fn _ => prove_eqvt_tac thy orig_thm pi' pi'') |>
diff -r 700ed1f4c576 -r 54758ca53fd6 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Fri Aug 28 17:07:15 2009 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Aug 28 18:18:30 2009 +0200
@@ -29,30 +29,30 @@
 val bT = HOLogic.boolT;
 val dest_numeral = HOLogic.dest_number #> snd;
 
-val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] = 
+val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] =
     map(instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"};
 
-val [infDconj, infDdisj, infDdvd,infDndvd,infDP] = 
+val [infDconj, infDdisj, infDdvd,infDndvd,infDP] =
     map(instantiate' [SOME @{ctyp "int"}] []) @{thms "inf_period"};
 
-val [piconj, pidisj, pieq,pineq,pilt,pile,pigt,pige,pidvd,pindvd,piP] = 
+val [piconj, pidisj, pieq,pineq,pilt,pile,pigt,pige,pidvd,pindvd,piP] =
     map (instantiate' [SOME @{ctyp "int"}] []) @{thms "pinf"};
 
 val [miP, piP] = map (instantiate' [SOME @{ctyp "bool"}] []) [miP, piP];
 
 val infDP = instantiate' (map SOME [@{ctyp "int"}, @{ctyp "bool"}]) [] infDP;
 
-val [[asetconj, asetdisj, aseteq, asetneq, asetlt, asetle, 
+val [[asetconj, asetdisj, aseteq, asetneq, asetlt, asetle,
       asetgt, asetge, asetdvd, asetndvd,asetP],
-     [bsetconj, bsetdisj, bseteq, bsetneq, bsetlt, bsetle, 
+     [bsetconj, bsetdisj, bseteq, bsetneq, bsetlt, bsetle,
       bsetgt, bsetge, bsetdvd, bsetndvd,bsetP]]  = [@{thms "aset"}, @{thms "bset"}];
 
-val [miex, cpmi, piex, cppi] = [@{thm "minusinfinity"}, @{thm "cpmi"}, 
+val [miex, cpmi, piex, cppi] = [@{thm "minusinfinity"}, @{thm "cpmi"},
                                 @{thm "plusinfinity"}, @{thm "cppi"}];
 
 val unity_coeff_ex = instantiate' [SOME @{ctyp "int"}] [] @{thm "unity_coeff_ex"};
 
-val [zdvd_mono,simp_from_to,all_not_ex] = 
+val [zdvd_mono,simp_from_to,all_not_ex] =
      [@{thm "zdvd_mono"}, @{thm "simp_from_to"}, @{thm "all_not_ex"}];
 
 val [dvd_uminus, dvd_uminus'] = @{thms "uminus_dvd_conv"};
@@ -62,49 +62,49 @@
 
 (* recognising cterm without moving to terms *)
 
-datatype fm = And of cterm*cterm| Or of cterm*cterm| Eq of cterm | NEq of cterm 
+datatype fm = And of cterm*cterm| Or of cterm*cterm| Eq of cterm | NEq of cterm
             | Lt of cterm | Le of cterm | Gt of cterm | Ge of cterm
             | Dvd of cterm*cterm | NDvd of cterm*cterm | Nox
 
-fun whatis x ct = 
-( case (term_of ct) of 
+fun whatis x ct =
+( case (term_of ct) of
   Const("op &",_)$_$_ => And (Thm.dest_binop ct)
 | Const ("op |",_)$_$_ => Or (Thm.dest_binop ct)
 | Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
-| Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) => 
+| Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) =>
   if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
 | Const (@{const_name HOL.less}, _) $ y$ z =>
-   if term_of x aconv y then Lt (Thm.dest_arg ct) 
+   if term_of x aconv y then Lt (Thm.dest_arg ct)
    else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox
-| Const (@{const_name HOL.less_eq}, _) $ y $ z => 
-   if term_of x aconv y then Le (Thm.dest_arg ct) 
+| Const (@{const_name HOL.less_eq}, _) $ y $ z =>
+   if term_of x aconv y then Le (Thm.dest_arg ct)
    else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
 | Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_) =>
-   if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox 
+   if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox
 | Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_)) =>
-   if term_of x aconv y then 
-   NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox 
+   if term_of x aconv y then
+   NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox
 | _ => Nox)
-  handle CTERM _ => Nox; 
+  handle CTERM _ => Nox;
 
-fun get_pmi_term t = 
-  let val (x,eq) = 
+fun get_pmi_term t =
+  let val (x,eq) =
      (Thm.dest_abs NONE o Thm.dest_arg o snd o Thm.dest_abs NONE o Thm.dest_arg)
         (Thm.dest_arg t)
 in (Thm.cabs x o Thm.dest_arg o Thm.dest_arg) eq end;
 
 val get_pmi = get_pmi_term o cprop_of;
 
-val p_v' = @{cpat "?P' :: int => bool"}; 
+val p_v' = @{cpat "?P' :: int => bool"};
 val q_v' = @{cpat "?Q' :: int => bool"};
 val p_v = @{cpat "?P:: int => bool"};
 val q_v = @{cpat "?Q:: int => bool"};
 
-fun myfwd (th1, th2, th3) p q 
-      [(th_1,th_2,th_3), (th_1',th_2',th_3')] = 
-  let  
+fun myfwd (th1, th2, th3) p q
+      [(th_1,th_2,th_3), (th_1',th_2',th_3')] =
+  let
    val (mp', mq') = (get_pmi th_1, get_pmi th_1')
-   val mi_th = FWD (instantiate ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1) 
+   val mi_th = FWD (instantiate ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1)
                    [th_1, th_1']
    val infD_th = FWD (instantiate ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3']
    val set_th = FWD (instantiate ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2']
@@ -123,15 +123,15 @@
 val [addC, mulC, subC, negC] = map term_of [cadd, cmulC, cminus, cneg]
 val [zero, one] = [@{term "0 :: int"}, @{term "1 :: int"}];
 
-val is_numeral = can dest_numeral; 
+val is_numeral = can dest_numeral;
 
-fun numeral1 f n = HOLogic.mk_number iT (f (dest_numeral n)); 
+fun numeral1 f n = HOLogic.mk_number iT (f (dest_numeral n));
 fun numeral2 f m n = HOLogic.mk_number iT (f (dest_numeral m) (dest_numeral n));
 
-val [minus1,plus1] = 
+val [minus1,plus1] =
     map (fn c => fn t => Thm.capply (Thm.capply c t) cone) [cminus,cadd];
 
-fun decomp_pinf x dvd inS [aseteq, asetneq, asetlt, asetle, 
+fun decomp_pinf x dvd inS [aseteq, asetneq, asetlt, asetle,
                            asetgt, asetge,asetdvd,asetndvd,asetP,
                            infDdvd, infDndvd, asetconj,
                            asetdisj, infDconj, infDdisj] cp =
@@ -144,11 +144,11 @@
 | Le t => ([], K (inst' [t] pile, FWD (inst' [t] asetle) [inS (plus1 t)], infDFalse))
 | Gt t => ([], K (inst' [t] pigt, (inst' [t] asetgt), infDTrue))
 | Ge t => ([], K (inst' [t] pige, (inst' [t] asetge), infDTrue))
-| Dvd (d,s) => 
+| Dvd (d,s) =>
    ([],let val dd = dvd d
-	     in K (inst' [d,s] pidvd, FWD (inst' [d,s] asetdvd) [dd],FWD (inst' [d,s] infDdvd) [dd]) end)
+       in K (inst' [d,s] pidvd, FWD (inst' [d,s] asetdvd) [dd],FWD (inst' [d,s] infDdvd) [dd]) end)
 | NDvd(d,s) => ([],let val dd = dvd d
-	      in K (inst' [d,s] pindvd, FWD (inst' [d,s] asetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end)
+        in K (inst' [d,s] pindvd, FWD (inst' [d,s] asetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end)
 | _ => ([], K (inst' [cp] piP, inst' [cp] asetP, inst' [cp] infDP));
 
 fun decomp_minf x dvd inS [bseteq,bsetneq,bsetlt, bsetle, bsetgt,
@@ -165,82 +165,82 @@
 | Gt t => ([], K (inst' [t] migt, FWD (inst' [t] bsetgt) [inS t], infDFalse))
 | Ge t => ([], K (inst' [t] mige,FWD (inst' [t] bsetge) [inS (minus1 t)], infDFalse))
 | Dvd (d,s) => ([],let val dd = dvd d
-	      in K (inst' [d,s] midvd, FWD (inst' [d,s] bsetdvd) [dd] , FWD (inst' [d,s] infDdvd) [dd]) end)
+        in K (inst' [d,s] midvd, FWD (inst' [d,s] bsetdvd) [dd] , FWD (inst' [d,s] infDdvd) [dd]) end)
 | NDvd (d,s) => ([],let val dd = dvd d
-	      in K (inst' [d,s] mindvd, FWD (inst' [d,s] bsetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end)
+        in K (inst' [d,s] mindvd, FWD (inst' [d,s] bsetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end)
 | _ => ([], K (inst' [cp] miP, inst' [cp] bsetP, inst' [cp] infDP))
 
     (* Canonical linear form for terms, formulae etc.. *)
-fun provelin ctxt t = Goal.prove ctxt [] [] t 
+fun provelin ctxt t = Goal.prove ctxt [] [] t
   (fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]);
-fun linear_cmul 0 tm = zero 
-  | linear_cmul n tm = case tm of  
+fun linear_cmul 0 tm = zero
+  | linear_cmul n tm = case tm of
       Const (@{const_name HOL.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
     | Const (@{const_name HOL.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x
     | Const (@{const_name HOL.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b
     | (m as Const (@{const_name HOL.uminus}, _)) $ a => m $ linear_cmul n a
     | _ => numeral1 (fn m => n * m) tm;
-fun earlier [] x y = false 
-	| earlier (h::t) x y = 
-    if h aconv y then false else if h aconv x then true else earlier t x y; 
+fun earlier [] x y = false
+  | earlier (h::t) x y =
+    if h aconv y then false else if h aconv x then true else earlier t x y;
 
-fun linear_add vars tm1 tm2 = case (tm1, tm2) of 
+fun linear_add vars tm1 tm2 = case (tm1, tm2) of
     (Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c1 $ x1) $ r1,
     Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) =>
-   if x1 = x2 then 
+   if x1 = x2 then
      let val c = numeral2 (curry op +) c1 c2
       in if c = zero then linear_add vars r1 r2
          else addC$(mulC$c$x1)$(linear_add vars r1 r2)
-     end 
+     end
      else if earlier vars x1 x2 then addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
    else addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
  | (Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c1 $ x1) $ r1, _) =>
       addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
- | (_, Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) => 
+ | (_, Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) =>
       addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
  | (_, _) => numeral2 (curry op +) tm1 tm2;
- 
-fun linear_neg tm = linear_cmul ~1 tm; 
-fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2); 
+
+fun linear_neg tm = linear_cmul ~1 tm;
+fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);
 
 
-fun lint vars tm =  if is_numeral tm then tm  else case tm of 
+fun lint vars tm =  if is_numeral tm then tm  else case tm of
   Const (@{const_name HOL.uminus}, _) $ t => linear_neg (lint vars t)
 | Const (@{const_name HOL.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
 | Const (@{const_name HOL.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
 | Const (@{const_name HOL.times}, _) $ s $ t =>
-  let val s' = lint vars s  
-      val t' = lint vars t  
-  in if is_numeral s' then (linear_cmul (dest_numeral s') t') 
-     else if is_numeral t' then (linear_cmul (dest_numeral t') s') 
+  let val s' = lint vars s
+      val t' = lint vars t
+  in if is_numeral s' then (linear_cmul (dest_numeral s') t')
+     else if is_numeral t' then (linear_cmul (dest_numeral t') s')
      else raise COOPER ("Cooper Failed", TERM ("lint: not linear",[tm]))
-  end 
+  end
  | _ => addC $ (mulC $ one $ tm) $ zero;
 
-fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.less}, T) $ s $ t)) = 
+fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.less}, T) $ s $ t)) =
     lin vs (Const (@{const_name HOL.less_eq}, T) $ t $ s)
-  | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name HOL.less_eq}, T) $ s $ t)) = 
+  | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name HOL.less_eq}, T) $ s $ t)) =
     lin vs (Const (@{const_name HOL.less}, T) $ t $ s)
   | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
-  | lin (vs as x::_) (Const(@{const_name Ring_and_Field.dvd},_)$d$t) = 
+  | lin (vs as x::_) (Const(@{const_name Ring_and_Field.dvd},_)$d$t) =
     HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} (numeral1 abs d, lint vs t)
-  | lin (vs as x::_) ((b as Const("op =",_))$s$t) = 
-     (case lint vs (subC$t$s) of 
-      (t as a$(m$c$y)$r) => 
+  | lin (vs as x::_) ((b as Const("op =",_))$s$t) =
+     (case lint vs (subC$t$s) of
+      (t as a$(m$c$y)$r) =>
         if x <> y then b$zero$t
         else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r
         else b$(m$c$y)$(linear_neg r)
       | t => b$zero$t)
-  | lin (vs as x::_) (b$s$t) = 
-     (case lint vs (subC$t$s) of 
-      (t as a$(m$c$y)$r) => 
+  | lin (vs as x::_) (b$s$t) =
+     (case lint vs (subC$t$s) of
+      (t as a$(m$c$y)$r) =>
         if x <> y then b$zero$t
         else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r
         else b$(linear_neg r)$(m$c$y)
       | t => b$zero$t)
   | lin vs fm = fm;
 
-fun lint_conv ctxt vs ct = 
+fun lint_conv ctxt vs ct =
 let val t = term_of ct
 in (provelin ctxt ((HOLogic.eq_const iT)$t$(lint vs t) |> HOLogic.mk_Trueprop))
              RS eq_reflection
@@ -251,26 +251,26 @@
 fun is_intrel (b$_$_) = is_intrel_type (fastype_of b)
   | is_intrel (@{term "Not"}$(b$_$_)) = is_intrel_type (fastype_of b)
   | is_intrel _ = false;
- 
+
 fun linearize_conv ctxt vs ct = case term_of ct of
-  Const(@{const_name Ring_and_Field.dvd},_)$d$t => 
-  let 
+  Const(@{const_name Ring_and_Field.dvd},_)$d$t =>
+  let
     val th = binop_conv (lint_conv ctxt vs) ct
     val (d',t') = Thm.dest_binop (Thm.rhs_of th)
     val (dt',tt') = (term_of d', term_of t')
-  in if is_numeral dt' andalso is_numeral tt' 
+  in if is_numeral dt' andalso is_numeral tt'
      then Conv.fconv_rule (arg_conv (Simplifier.rewrite presburger_ss)) th
-     else 
-     let 
-      val dth = 
-      ((if dest_numeral (term_of d') < 0 then 
+     else
+     let
+      val dth =
+      ((if dest_numeral (term_of d') < 0 then
           Conv.fconv_rule (arg_conv (arg1_conv (lint_conv ctxt vs)))
                            (Thm.transitive th (inst' [d',t'] dvd_uminus))
         else th) handle TERM _ => th)
       val d'' = Thm.rhs_of dth |> Thm.dest_arg1
      in
-      case tt' of 
-        Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$_)$_ => 
+      case tt' of
+        Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$_)$_ =>
         let val x = dest_numeral c
         in if x < 0 then Conv.fconv_rule (arg_conv (arg_conv (lint_conv ctxt vs)))
                                        (Thm.transitive dth (inst' [d'',t'] dvd_uminus'))
@@ -279,29 +279,29 @@
      end
   end
 | Const (@{const_name Not},_)$(Const(@{const_name Ring_and_Field.dvd},_)$_$_) => arg_conv (linearize_conv ctxt vs) ct
-| t => if is_intrel t 
+| t => if is_intrel t
       then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop))
        RS eq_reflection
       else reflexive ct;
 
 val dvdc = @{cterm "op dvd :: int => _"};
 
-fun unify ctxt q = 
+fun unify ctxt q =
  let
   val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs NONE
-  val x = term_of cx 
+  val x = term_of cx
   val ins = insert (op = : int * int -> bool)
-  fun h (acc,dacc) t = 
+  fun h (acc,dacc) t =
    case (term_of t) of
-    Const(s,_)$(Const(@{const_name HOL.times},_)$c$y)$ _ => 
+    Const(s,_)$(Const(@{const_name HOL.times},_)$c$y)$ _ =>
     if x aconv y andalso member (op =)
       ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
     then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
-  | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) => 
+  | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) =>
     if x aconv y andalso member (op =)
-       [@{const_name HOL.less}, @{const_name HOL.less_eq}] s 
+       [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
     then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
-  | Const(@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_) => 
+  | Const(@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_) =>
     if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
   | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
@@ -309,51 +309,53 @@
   | _ => (acc, dacc)
   val (cs,ds) = h ([],[]) p
   val l = Integer.lcms (cs union ds)
-  fun cv k ct = 
-    let val (tm as b$s$t) = term_of ct 
+  fun cv k ct =
+    let val (tm as b$s$t) = term_of ct
     in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t))
          |> HOLogic.mk_Trueprop |> provelin ctxt) RS eq_reflection end
-  fun nzprop x = 
-   let 
-    val th = 
-     Simplifier.rewrite lin_ss 
-      (Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"} 
-           (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x)) 
+  fun nzprop x =
+   let
+    val th =
+     Simplifier.rewrite lin_ss
+      (Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"}
+           (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x))
            @{cterm "0::int"})))
    in equal_elim (Thm.symmetric th) TrueI end;
-  val notz = let val tab = fold Inttab.update 
-                               (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty 
-            in 
-             (fn ct => (valOf (Inttab.lookup tab (ct |> term_of |> dest_numeral)) 
-                handle Option => (writeln "noz: Theorems-Table contains no entry for"; 
-                                    Display.print_cterm ct ; raise Option)))
-           end
-  fun unit_conv t = 
+  val notz =
+    let val tab = fold Inttab.update
+          (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty
+    in
+      fn ct => valOf (Inttab.lookup tab (ct |> term_of |> dest_numeral))
+        handle Option =>
+          (writeln ("noz: Theorems-Table contains no entry for " ^
+              Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
+    end
+  fun unit_conv t =
    case (term_of t) of
    Const("op &",_)$_$_ => binop_conv unit_conv t
   | Const("op |",_)$_$_ => binop_conv unit_conv t
   | Const (@{const_name Not},_)$_ => arg_conv unit_conv t
-  | Const(s,_)$(Const(@{const_name HOL.times},_)$c$y)$ _ => 
+  | Const(s,_)$(Const(@{const_name HOL.times},_)$c$y)$ _ =>
     if x=y andalso member (op =)
       ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
     then cv (l div dest_numeral c) t else Thm.reflexive t
-  | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) => 
+  | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) =>
     if x=y andalso member (op =)
       [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
     then cv (l div dest_numeral c) t else Thm.reflexive t
-  | Const(@{const_name Ring_and_Field.dvd},_)$d$(r as (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_)) => 
-    if x=y then 
-      let 
+  | Const(@{const_name Ring_and_Field.dvd},_)$d$(r as (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_)) =>
+    if x=y then
+      let
        val k = l div dest_numeral c
        val kt = HOLogic.mk_number iT k
-       val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t] 
+       val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t]
              ((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono)
        val (d',t') = (mulC$kt$d, mulC$kt$r)
        val thc = (provelin ctxt ((HOLogic.eq_const iT)$d'$(lint [] d') |> HOLogic.mk_Trueprop))
                    RS eq_reflection
        val tht = (provelin ctxt ((HOLogic.eq_const iT)$t'$(linear_cmul k r) |> HOLogic.mk_Trueprop))
                  RS eq_reflection
-      in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule dvdc thc) tht) end                 
+      in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule dvdc thc) tht) end
     else Thm.reflexive t
   | _ => Thm.reflexive t
   val uth = unit_conv p
@@ -361,7 +363,7 @@
   val ltx = Thm.capply (Thm.capply cmulC clt) cx
   val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth)
   val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex
-  val thf = transitive th 
+  val thf = transitive th
       (transitive (symmetric (beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th')
   val (lth,rth) = Thm.dest_comb (cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true
                   ||> beta_conversion true |>> Thm.symmetric
@@ -374,25 +376,25 @@
 fun mkISet cts = fold_rev (Thm.capply insert_tm #> Thm.capply) cts emptyIS;
 val cTrp = @{cterm "Trueprop"};
 val eqelem_imp_imp = (thm"eqelem_imp_iff") RS iffD1;
-val [A_tm,B_tm] = map (fn th => cprop_of th |> funpow 2 Thm.dest_arg |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg 
+val [A_tm,B_tm] = map (fn th => cprop_of th |> funpow 2 Thm.dest_arg |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg
                                       |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg)
                       [asetP,bsetP];
 
 val D_tm = @{cpat "?D::int"};
 
-fun cooperex_conv ctxt vs q = 
-let 
+fun cooperex_conv ctxt vs q =
+let
 
  val uth = unify ctxt q
  val (x,p) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of uth))
  val ins = insert (op aconvc)
- fun h t (bacc,aacc,dacc) = 
+ fun h t (bacc,aacc,dacc) =
   case (whatis x t) of
     And (p,q) => h q (h p (bacc,aacc,dacc))
   | Or (p,q) => h q  (h p (bacc,aacc,dacc))
-  | Eq t => (ins (minus1 t) bacc, 
+  | Eq t => (ins (minus1 t) bacc,
              ins (plus1 t) aacc,dacc)
-  | NEq t => (ins t bacc, 
+  | NEq t => (ins t bacc,
               ins t aacc, dacc)
   | Lt t => (bacc, ins t aacc, dacc)
   | Le t => (bacc, ins (plus1 t) aacc,dacc)
@@ -405,89 +407,92 @@
  val d = Integer.lcms ds
  val cd = Numeral.mk_cnumber @{ctyp "int"} d
  val dt = term_of cd
- fun divprop x = 
-   let 
-    val th = 
-     Simplifier.rewrite lin_ss 
-      (Thm.capply @{cterm Trueprop} 
+ fun divprop x =
+   let
+    val th =
+     Simplifier.rewrite lin_ss
+      (Thm.capply @{cterm Trueprop}
            (Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
    in equal_elim (Thm.symmetric th) TrueI end;
- val dvd = let val tab = fold Inttab.update
-                               (ds ~~ (map divprop ds)) Inttab.empty in 
-           (fn ct => (valOf (Inttab.lookup tab (term_of ct |> dest_numeral)) 
-                    handle Option => (writeln "dvd: Theorems-Table contains no entry for"; 
-                                      Display.print_cterm ct ; raise Option)))
-           end
- val dp = 
-   let val th = Simplifier.rewrite lin_ss 
-      (Thm.capply @{cterm Trueprop} 
+ val dvd =
+   let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
+     fn ct => valOf (Inttab.lookup tab (term_of ct |> dest_numeral))
+       handle Option =>
+        (writeln ("dvd: Theorems-Table contains no entry for" ^
+            Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
+   end
+ val dp =
+   let val th = Simplifier.rewrite lin_ss
+      (Thm.capply @{cterm Trueprop}
            (Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd))
    in equal_elim (Thm.symmetric th) TrueI end;
     (* A and B set *)
-   local 
+   local
      val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"}
      val insI2 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI2"}
    in
-    fun provein x S = 
+    fun provein x S =
      case term_of S of
         Const(@{const_name Orderings.bot}, _) => error "Unexpected error in Cooper, please email Amine Chaieb"
-      | Const(@{const_name insert}, _) $ y $ _ => 
+      | Const(@{const_name insert}, _) $ y $ _ =>
          let val (cy,S') = Thm.dest_binop S
          in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
-         else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2) 
+         else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
                            (provein x S')
          end
    end
- 
+
  val al = map (lint vs o term_of) a0
  val bl = map (lint vs o term_of) b0
- val (sl,s0,f,abths,cpth) = 
-   if length (distinct (op aconv) bl) <= length (distinct (op aconv) al) 
-   then  
+ val (sl,s0,f,abths,cpth) =
+   if length (distinct (op aconv) bl) <= length (distinct (op aconv) al)
+   then
     (bl,b0,decomp_minf,
-     fn B => (map (fn th => implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp) 
+     fn B => (map (fn th => implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp)
                      [bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@
-                   (map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)])) 
+                   (map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]))
                         [bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj,
                          bsetdisj,infDconj, infDdisj]),
-                       cpmi) 
-     else (al,a0,decomp_pinf,fn A => 
+                       cpmi)
+     else (al,a0,decomp_pinf,fn A =>
           (map (fn th => implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp)
                    [aseteq,asetneq,asetlt, asetle, asetgt,asetge])@
-                   (map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)])) 
+                   (map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]))
                    [asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj,
                          asetdisj,infDconj, infDdisj]),cppi)
- val cpth = 
+ val cpth =
   let
-   val sths = map (fn (tl,t0) => 
-                      if tl = term_of t0 
+   val sths = map (fn (tl,t0) =>
+                      if tl = term_of t0
                       then instantiate' [SOME @{ctyp "int"}] [SOME t0] refl
-                      else provelin ctxt ((HOLogic.eq_const iT)$tl$(term_of t0) 
-                                 |> HOLogic.mk_Trueprop)) 
+                      else provelin ctxt ((HOLogic.eq_const iT)$tl$(term_of t0)
+                                 |> HOLogic.mk_Trueprop))
                    (sl ~~ s0)
    val csl = distinct (op aconvc) (map (cprop_of #> Thm.dest_arg #> Thm.dest_arg1) sths)
    val S = mkISet csl
-   val inStab = fold (fn ct => fn tab => Termtab.update (term_of ct, provein ct S) tab) 
+   val inStab = fold (fn ct => fn tab => Termtab.update (term_of ct, provein ct S) tab)
                     csl Termtab.empty
    val eqelem_th = instantiate' [SOME @{ctyp "int"}] [NONE,NONE, SOME S] eqelem_imp_imp
-   val inS = 
-     let 
-      fun transmem th0 th1 = 
-       Thm.equal_elim 
-        (Drule.arg_cong_rule cTrp (Drule.fun_cong_rule (Drule.arg_cong_rule 
+   val inS =
+     let
+      fun transmem th0 th1 =
+       Thm.equal_elim
+        (Drule.arg_cong_rule cTrp (Drule.fun_cong_rule (Drule.arg_cong_rule
                ((Thm.dest_fun o Thm.dest_fun o Thm.dest_arg o cprop_of) th1) th0) S)) th1
       val tab = fold Termtab.update
-        (map (fn eq => 
-                let val (s,t) = cprop_of eq |> Thm.dest_arg |> Thm.dest_binop 
-                    val th = if term_of s = term_of t 
+        (map (fn eq =>
+                let val (s,t) = cprop_of eq |> Thm.dest_arg |> Thm.dest_binop
+                    val th = if term_of s = term_of t
                              then valOf(Termtab.lookup inStab (term_of s))
-                             else FWD (instantiate' [] [SOME s, SOME t] eqelem_th) 
+                             else FWD (instantiate' [] [SOME s, SOME t] eqelem_th)
                                 [eq, valOf(Termtab.lookup inStab (term_of s))]
                  in (term_of t, th) end)
                   sths) Termtab.empty
-        in fn ct => 
-          (valOf (Termtab.lookup tab (term_of ct))
-           handle Option => (writeln "inS: No theorem for " ; Display.print_cterm ct ; raise Option))
+        in
+          fn ct => valOf (Termtab.lookup tab (term_of ct))
+            handle Option =>
+              (writeln ("inS: No theorem for " ^ Syntax.string_of_term ctxt (Thm.term_of ct));
+                raise Option)
         end
        val (inf, nb, pd) = divide_and_conquer (f x dvd inS (abths S)) p
    in [dp, inf, nb, pd] MRS cpth
@@ -496,9 +501,9 @@
 in Thm.transitive cpth' ((simp_thms_conv ctxt then_conv eval_conv) (Thm.rhs_of cpth'))
 end;
 
-fun literals_conv bops uops env cv = 
+fun literals_conv bops uops env cv =
  let fun h t =
-  case (term_of t) of 
+  case (term_of t) of
    b$_$_ => if member (op aconv) bops b then binop_conv h t else cv env t
  | u$_ => if member (op aconv) uops u then arg_conv h t else cv env t
  | _ => cv env t
@@ -508,21 +513,21 @@
  nnf_conv then_conv literals_conv [HOLogic.conj, HOLogic.disj] [] env (linearize_conv ctxt);
 
 local
- val pcv = Simplifier.rewrite 
-     (HOL_basic_ss addsimps (simp_thms @ (List.take(ex_simps,4)) 
+ val pcv = Simplifier.rewrite
+     (HOL_basic_ss addsimps (simp_thms @ (List.take(ex_simps,4))
                       @ [not_all,all_not_ex, ex_disj_distrib]))
  val postcv = Simplifier.rewrite presburger_ss
- fun conv ctxt p = 
+ fun conv ctxt p =
   let val _ = ()
   in
-   Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of) 
-      (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt) 
-      (cooperex_conv ctxt) p 
+   Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of)
+      (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
+      (cooperex_conv ctxt) p
   end
   handle  CTERM s => raise COOPER ("Cooper Failed", CTERM s)
-        | THM s => raise COOPER ("Cooper Failed", THM s) 
-        | TYPE s => raise COOPER ("Cooper Failed", TYPE s) 
-in val cooper_conv = conv 
+        | THM s => raise COOPER ("Cooper Failed", THM s)
+        | TYPE s => raise COOPER ("Cooper Failed", TYPE s)
+in val cooper_conv = conv
 end;
 end;
 
@@ -544,12 +549,12 @@
   | Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t')
   | Const(@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
   | Const(@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
-  | Const(@{const_name HOL.times},_)$t1$t2 => 
+  | Const(@{const_name HOL.times},_)$t1$t2 =>
      (Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
-    handle TERM _ => 
+    handle TERM _ =>
        (Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1)
         handle TERM _ => cooper "Reification: Unsupported kind of multiplication"))
-  | _ => (C (HOLogic.dest_number t |> snd) 
+  | _ => (C (HOLogic.dest_number t |> snd)
            handle TERM _ => cooper "Reification: unknown term");
 
 fun qf_of_term ps vs t =  case t
@@ -557,7 +562,7 @@
   | Const("False",_) => F
   | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
   | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
-  | Const(@{const_name Ring_and_Field.dvd},_)$t1$t2 => 
+  | Const(@{const_name Ring_and_Field.dvd},_)$t1$t2 =>
       (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")  (* FIXME avoid handle _ *)
   | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
   | @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
@@ -565,42 +570,42 @@
   | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
   | Const("op -->",_)$t1$t2 => Imp(qf_of_term ps vs t1,qf_of_term ps vs t2)
   | Const (@{const_name Not},_)$t' => Not(qf_of_term ps vs t')
-  | Const("Ex",_)$Abs(xn,xT,p) => 
+  | Const("Ex",_)$Abs(xn,xT,p) =>
      let val (xn',p') = variant_abs (xn,xT,p)
          val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
      in E (qf_of_term ps vs' p')
      end
-  | Const("All",_)$Abs(xn,xT,p) => 
+  | Const("All",_)$Abs(xn,xT,p) =>
      let val (xn',p') = variant_abs (xn,xT,p)
          val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
      in A (qf_of_term ps vs' p')
      end
-  | _ =>(case AList.lookup (op aconv) ps t of 
+  | _ =>(case AList.lookup (op aconv) ps t of
            NONE => cooper "Reification: unknown term!"
          | SOME n => Closed n);
 
 local
  val ops = [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
-             @{term "op = :: int => _"}, @{term "op < :: int => _"}, 
-             @{term "op <= :: int => _"}, @{term "Not"}, @{term "All:: (int => _) => _"}, 
+             @{term "op = :: int => _"}, @{term "op < :: int => _"},
+             @{term "op <= :: int => _"}, @{term "Not"}, @{term "All:: (int => _) => _"},
              @{term "Ex:: (int => _) => _"}, @{term "True"}, @{term "False"}]
 fun ty t = Bool.not (fastype_of t = HOLogic.boolT)
 in
 fun term_bools acc t =
-case t of 
-    (l as f $ a) $ b => if ty t orelse f mem ops then term_bools (term_bools acc l)b 
+case t of
+    (l as f $ a) $ b => if ty t orelse f mem ops then term_bools (term_bools acc l)b
             else insert (op aconv) t acc
-  | f $ a => if ty t orelse f mem ops then term_bools (term_bools acc f) a  
+  | f $ a => if ty t orelse f mem ops then term_bools (term_bools acc f) a
             else insert (op aconv) t acc
   | Abs p => term_bools acc (snd (variant_abs p))
   | _ => if ty t orelse t mem ops then acc else insert (op aconv) t acc
 end;
- 
+
 fun myassoc2 l v =
     case l of
-	[] => NONE
+  [] => NONE
       | (x,v')::xs => if v = v' then SOME x
-		      else myassoc2 xs v;
+          else myassoc2 xs v;
 
 fun term_of_i vs t = case t
  of C i => HOLogic.mk_number HOLogic.intT i
@@ -612,9 +617,9 @@
       HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2
   | Cn (n, i, t') => term_of_i vs (Add (Mul (i, Bound n), t'));
 
-fun term_of_qf ps vs t = 
- case t of 
-   T => HOLogic.true_const 
+fun term_of_qf ps vs t =
+ case t of
+   T => HOLogic.true_const
  | F => HOLogic.false_const
  | Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
  | Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"}
@@ -622,7 +627,7 @@
  | Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
  | Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
  | NEq t' => term_of_qf ps vs (Not (Eq t'))
- | Dvd(i,t') => @{term "op dvd :: int => _ "} $ 
+ | Dvd(i,t') => @{term "op dvd :: int => _ "} $
     HOLogic.mk_number HOLogic.intT i $ term_of_i vs t'
  | NDvd(i,t')=> term_of_qf ps vs (Not(Dvd(i,t')))
  | Not t' => HOLogic.Not$(term_of_qf ps vs t')
diff -r 700ed1f4c576 -r 54758ca53fd6 src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Fri Aug 28 17:07:15 2009 +0200
+++ b/src/HOL/Tools/TFL/rules.ML	Fri Aug 28 18:18:30 2009 +0200
@@ -544,7 +544,7 @@
 (*---------------------------------------------------------------------------
  * Trace information for the rewriter
  *---------------------------------------------------------------------------*)
-val term_ref = ref[] : term list ref
+val term_ref = ref [] : term list ref
 val ss_ref = ref [] : simpset list ref;
 val thm_ref = ref [] : thm list ref;
 val tracing = ref false;
@@ -554,8 +554,8 @@
 fun print_thms s L =
   say (cat_lines (s :: map Display.string_of_thm_without_context L));
 
-fun print_cterms s L =
-  say (cat_lines (s :: map Display.string_of_cterm L));
+fun print_cterm s ct =
+  say (cat_lines [s, Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct)]);
 
 
 (*---------------------------------------------------------------------------
@@ -683,7 +683,7 @@
              (* Unquantified eliminate *)
              fun uq_eliminate (thm,imp,thy) =
                  let val tych = cterm_of thy
-                     val dummy = print_cterms "To eliminate:" [tych imp]
+                     val dummy = print_cterm "To eliminate:" (tych imp)
                      val ants = map tych (Logic.strip_imp_prems imp)
                      val eq = Logic.strip_imp_concl imp
                      val lhs = tych(get_lhs eq)
@@ -781,9 +781,8 @@
               val antl = case rcontext of [] => []
                          | _   => [S.list_mk_conj(map cncl rcontext)]
               val TC = genl(S.list_mk_imp(antl, A))
-              val dummy = print_cterms "func:" [cterm_of thy func]
-              val dummy = print_cterms "TC:"
-                              [cterm_of thy (HOLogic.mk_Trueprop TC)]
+              val dummy = print_cterm "func:" (cterm_of thy func)
+              val dummy = print_cterm "TC:" (cterm_of thy (HOLogic.mk_Trueprop TC))
               val dummy = tc_list := (TC :: !tc_list)
               val nestedp = isSome (S.find_term is_func TC)
               val dummy = if nestedp then say "nested" else say "not_nested"