src/HOL/Tools/hologic.ML
changeset 32339 40612b7ace87
parent 32287 65d5c5b30747
child 32342 3fabf5b5fc83
     1.1 --- a/src/HOL/Tools/hologic.ML	Thu Jul 30 08:18:22 2009 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Thu Jul 30 13:52:17 2009 +0200
     1.3 @@ -118,6 +118,8 @@
     1.4    val mk_literal: string -> term
     1.5    val dest_literal: term -> string
     1.6    val mk_typerep: typ -> term
     1.7 +  val termT: typ
     1.8 +  val term_of_const: typ -> term
     1.9    val mk_term_of: typ -> term -> term
    1.10    val reflect_term: term -> term
    1.11    val mk_valtermify_app: string -> (string * typ) list -> typ -> term
    1.12 @@ -591,7 +593,9 @@
    1.13  
    1.14  val termT = Type ("Code_Eval.term", []);
    1.15  
    1.16 -fun mk_term_of T t = Const ("Code_Eval.term_of_class.term_of", T --> termT) $ t;
    1.17 +fun term_of_const T = Const ("Code_Eval.term_of_class.term_of", T --> termT);
    1.18 +
    1.19 +fun mk_term_of T t = term_of_const T $ t;
    1.20  
    1.21  fun reflect_term (Const (c, T)) =
    1.22        Const ("Code_Eval.Const", literalT --> typerepT --> termT)