src/HOL/Tools/hologic.ML
changeset 32657 5f13912245ff
parent 32446 cde4f2c8bdd5
child 33245 65232054ffd0
     1.1 --- a/src/HOL/Tools/hologic.ML	Wed Sep 23 13:42:53 2009 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Wed Sep 23 14:00:12 2009 +0200
     1.3 @@ -613,17 +613,17 @@
     1.4    | mk_typerep (T as TFree _) = Const ("Typerep.typerep_class.typerep",
     1.5        Term.itselfT T --> typerepT) $ Logic.mk_type T;
     1.6  
     1.7 -val termT = Type ("Code_Eval.term", []);
     1.8 +val termT = Type ("Code_Evaluation.term", []);
     1.9  
    1.10 -fun term_of_const T = Const ("Code_Eval.term_of_class.term_of", T --> termT);
    1.11 +fun term_of_const T = Const ("Code_Evaluation.term_of_class.term_of", T --> termT);
    1.12  
    1.13  fun mk_term_of T t = term_of_const T $ t;
    1.14  
    1.15  fun reflect_term (Const (c, T)) =
    1.16 -      Const ("Code_Eval.Const", literalT --> typerepT --> termT)
    1.17 +      Const ("Code_Evaluation.Const", literalT --> typerepT --> termT)
    1.18          $ mk_literal c $ mk_typerep T
    1.19    | reflect_term (t1 $ t2) =
    1.20 -      Const ("Code_Eval.App", termT --> termT --> termT)
    1.21 +      Const ("Code_Evaluation.App", termT --> termT --> termT)
    1.22          $ reflect_term t1 $ reflect_term t2
    1.23    | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t)
    1.24    | reflect_term t = t;
    1.25 @@ -631,7 +631,7 @@
    1.26  fun mk_valtermify_app c vs T =
    1.27    let
    1.28      fun termifyT T = mk_prodT (T, unitT --> termT);
    1.29 -    fun valapp T T' = Const ("Code_Eval.valapp",
    1.30 +    fun valapp T T' = Const ("Code_Evaluation.valapp",
    1.31        termifyT (T --> T') --> termifyT T --> termifyT T');
    1.32      fun mk_fTs [] _ = []
    1.33        | mk_fTs (_ :: Ts) T = (Ts ---> T) :: mk_fTs Ts T;