# HG changeset patch
# User haftmann
# Date 1248954737 -7200
# Node ID 40612b7ace87e9d183892fedabdf140f111258a6
# Parent  c14aeb0bcce45fceca7f596a9ced4caa4ab51670
termT and term_of_const

diff -r c14aeb0bcce4 -r 40612b7ace87 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Thu Jul 30 08:18:22 2009 +0200
+++ b/src/HOL/Tools/hologic.ML	Thu Jul 30 13:52:17 2009 +0200
@@ -118,6 +118,8 @@
   val mk_literal: string -> term
   val dest_literal: term -> string
   val mk_typerep: typ -> term
+  val termT: typ
+  val term_of_const: typ -> term
   val mk_term_of: typ -> term -> term
   val reflect_term: term -> term
   val mk_valtermify_app: string -> (string * typ) list -> typ -> term
@@ -591,7 +593,9 @@
 
 val termT = Type ("Code_Eval.term", []);
 
-fun mk_term_of T t = Const ("Code_Eval.term_of_class.term_of", T --> termT) $ t;
+fun term_of_const T = Const ("Code_Eval.term_of_class.term_of", T --> termT);
+
+fun mk_term_of T t = term_of_const T $ t;
 
 fun reflect_term (Const (c, T)) =
       Const ("Code_Eval.Const", literalT --> typerepT --> termT)