the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils

--- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 14:29:04 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 16:29:56 2010 +0100
@@ -378,9 +378,7 @@
       | replace @{const True} = term_true
       | replace @{const False} = term_false
       | replace t = t
-  in
-    Term.map_aterms replace (HOLogic.dest_Trueprop (Thm.prop_of term_bool))
-  end
+  in Term.map_aterms replace (U.prop_of term_bool) end
 
 val fol_rules = [
   Let_def,
@@ -609,8 +607,7 @@
 
     val (builtins, ts1) =
       ithms
-      |> map (HOLogic.dest_Trueprop o Thm.prop_of o snd)
-      |> map (Envir.eta_contract o Envir.beta_norm)
+      |> map (Envir.beta_eta_contract o U.prop_of o snd)
       |> mark_builtins ctxt
 
     val ((dtyps, tr_context, ctxt1), ts2) =

--- a/src/HOL/Tools/SMT/smt_utils.ML	Wed Dec 15 14:29:04 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_utils.ML	Wed Dec 15 16:29:56 2010 +0100
@@ -47,6 +47,8 @@
   val mk_cprop: cterm -> cterm
   val dest_cprop: cterm -> cterm
   val mk_cequals: cterm -> cterm -> cterm
+  val term_of: cterm -> term
+  val prop_of: thm -> term
 
   (*conversions*)
   val if_conv: (term -> bool) -> conv -> conv -> conv
@@ -177,6 +179,10 @@
 val equals = mk_const_pat @{theory} @{const_name "=="} destT1
 fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
 
+val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
+fun term_of ct = dest_prop (Thm.term_of ct)
+fun prop_of thm = dest_prop (Thm.prop_of thm)
+
 
 (* conversions *)
 

--- a/src/HOL/Tools/SMT/z3_proof_literals.ML	Wed Dec 15 14:29:04 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_literals.ML	Wed Dec 15 16:29:56 2010 +0100
@@ -33,6 +33,7 @@
 structure Z3_Proof_Literals: Z3_PROOF_LITERALS =
 struct
 
+structure U = SMT_Utils
 structure T = Z3_Proof_Tools
 
 
@@ -41,10 +42,10 @@
 
 type littab = thm Termtab.table
 
-fun make_littab thms = fold (Termtab.update o `T.prop_of) thms Termtab.empty
+fun make_littab thms = fold (Termtab.update o `U.prop_of) thms Termtab.empty
 
-fun insert_lit thm = Termtab.update (`T.prop_of thm)
-fun delete_lit thm = Termtab.delete (T.prop_of thm)
+fun insert_lit thm = Termtab.update (`U.prop_of thm)
+fun delete_lit thm = Termtab.delete (U.prop_of thm)
 fun lookup_lit lits = Termtab.lookup lits
 fun get_first_lit f =
   Termtab.get_first (fn (t, thm) => if f t then SOME thm else NONE)
@@ -161,9 +162,9 @@
     val tab = fold (Termtab.update o rpair ()) stop_lits Termtab.empty
 
     fun explode1 thm =
-      if Termtab.defined tab (T.prop_of thm) then cons thm
+      if Termtab.defined tab (U.prop_of thm) then cons thm
       else
-        (case dest_rules (T.prop_of thm) of
+        (case dest_rules (U.prop_of thm) of
           SOME (rule1, rule2) =>
             explode2 rule1 thm #>
             explode2 rule2 thm #>
@@ -171,12 +172,12 @@
         | NONE => cons thm)
 
     and explode2 dest_rule thm =
-      if full orelse exists_lit is_conj (Termtab.defined tab) (T.prop_of thm)
+      if full orelse exists_lit is_conj (Termtab.defined tab) (U.prop_of thm)
       then explode1 (T.compose dest_rule thm)
       else cons (T.compose dest_rule thm)
 
     fun explode0 thm =
-      if not is_conj andalso is_dneg (T.prop_of thm)
+      if not is_conj andalso is_dneg (U.prop_of thm)
       then [T.compose dneg_rule thm]
       else explode1 thm []
 
@@ -284,7 +285,7 @@
   val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)}
   fun contra_left conj thm =
     let
-      val rules = explode_term conj (T.prop_of thm)
+      val rules = explode_term conj (U.prop_of thm)
       fun contra_lits (t, rs) =
         (case t of
           @{const Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)

--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed Dec 15 14:29:04 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed Dec 15 16:29:56 2010 +0100
@@ -15,6 +15,7 @@
 structure Z3_Proof_Reconstruction: Z3_PROOF_RECONSTRUCTION =
 struct
 
+structure U = SMT_Utils
 structure P = Z3_Proof_Parser
 structure T = Z3_Proof_Tools
 structure L = Z3_Proof_Literals
@@ -233,9 +234,9 @@
   fun lit_elim conj (p, idx) ct ptab =
     let val lits = literals_of p
     in
-      (case L.lookup_lit lits (T.term_of ct) of
+      (case L.lookup_lit lits (U.term_of ct) of
         SOME lit => (Thm lit, ptab)
-      | NONE => apfst Thm (derive conj (T.term_of ct) lits idx ptab))
+      | NONE => apfst Thm (derive conj (U.term_of ct) lits idx ptab))
     end
 in
 val and_elim = lit_elim true
@@ -266,7 +267,7 @@
   val explode_disj = L.explode false true false
   val join_disj = L.join false
   fun unit thm thms th =
-    let val t = @{const Not} $ T.prop_of thm and ts = map T.prop_of thms
+    let val t = @{const Not} $ U.prop_of thm and ts = map U.prop_of thms
     in join_disj (L.make_littab (thms @ explode_disj ts th)) t end
 
   fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
@@ -403,7 +404,7 @@
       named ctxt' "simp+fast" (T.by_tac simp_fast_tac))]
 in
 fun nnf ctxt vars ps ct =
-  (case T.term_of ct of
+  (case U.term_of ct of
     _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) =>
       if l aconv r
       then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))

--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Dec 15 14:29:04 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Dec 15 16:29:56 2010 +0100
@@ -6,9 +6,7 @@
 
 signature Z3_PROOF_TOOLS =
 sig
-  (*accessing and modifying terms*)
-  val term_of: cterm -> term
-  val prop_of: thm -> term
+  (*modifying terms*)
   val as_meta_eq: cterm -> cterm
 
   (*theorem nets*)
@@ -51,12 +49,7 @@
 
 
 
-(* accessing terms *)
-
-val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
-
-fun term_of ct = dest_prop (Thm.term_of ct)
-fun prop_of thm = dest_prop (Thm.prop_of thm)
+(* modifying terms *)
 
 fun as_meta_eq ct = uncurry U.mk_cequals (Thm.dest_binop (U.dest_cprop ct))