1.1 --- a/src/HOL/Code_Eval.thy	Wed Sep 23 13:42:53 2009 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,271 +0,0 @@
     1.4 -(*  Title:      HOL/Code_Eval.thy
     1.5 -    Author:     Florian Haftmann, TU Muenchen
     1.6 -*)
     1.7 -
     1.8 -header {* Term evaluation using the generic code generator *}
     1.9 -
    1.10 -theory Code_Eval
    1.11 -imports Plain Typerep Code_Numeral
    1.12 -begin
    1.13 -
    1.14 -subsection {* Term representation *}
    1.15 -
    1.16 -subsubsection {* Terms and class @{text term_of} *}
    1.17 -
    1.18 -datatype "term" = dummy_term
    1.19 -
    1.20 -definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
    1.21 -  "Const _ _ = dummy_term"
    1.22 -
    1.23 -definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
    1.24 -  "App _ _ = dummy_term"
    1.25 -
    1.26 -code_datatype Const App
    1.27 -
    1.28 -class term_of = typerep +
    1.29 -  fixes term_of :: "'a \<Rightarrow> term"
    1.30 -
    1.31 -lemma term_of_anything: "term_of x \<equiv> t"
    1.32 -  by (rule eq_reflection) (cases "term_of x", cases t, simp)
    1.33 -
    1.34 -definition valapp :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)
    1.35 -  \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
    1.36 -  "valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
    1.37 -
    1.38 -lemma valapp_code [code, code_unfold]:
    1.39 -  "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
    1.40 -  by (simp only: valapp_def fst_conv snd_conv)
    1.41 -
    1.42 -
    1.43 -subsubsection {* @{text term_of} instances *}
    1.44 -
    1.45 -instantiation "fun" :: (typerep, typerep) term_of
    1.46 -begin
    1.47 -
    1.48 -definition
    1.49 -  "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'')
    1.50 -     [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
    1.51 -
    1.52 -instance ..
    1.53 -
    1.54 -end
    1.55 -
    1.56 -setup {*
    1.57 -let
    1.58 -  fun add_term_of tyco raw_vs thy =
    1.59 -    let
    1.60 -      val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
    1.61 -      val ty = Type (tyco, map TFree vs);
    1.62 -      val lhs = Const (@{const_name term_of}, ty --> @{typ term})
    1.63 -        $ Free ("x", ty);
    1.64 -      val rhs = @{term "undefined \<Colon> term"};
    1.65 -      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    1.66 -      fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
    1.67 -        o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
    1.68 -    in
    1.69 -      thy
    1.70 -      |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
    1.71 -      |> `(fn lthy => Syntax.check_term lthy eq)
    1.72 -      |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
    1.73 -      |> snd
    1.74 -      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    1.75 -    end;
    1.76 -  fun ensure_term_of (tyco, (raw_vs, _)) thy =
    1.77 -    let
    1.78 -      val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
    1.79 -        andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
    1.80 -    in if need_inst then add_term_of tyco raw_vs thy else thy end;
    1.81 -in
    1.82 -  Code.type_interpretation ensure_term_of
    1.83 -end
    1.84 -*}
    1.85 -
    1.86 -setup {*
    1.87 -let
    1.88 -  fun mk_term_of_eq thy ty vs tyco (c, tys) =
    1.89 -    let
    1.90 -      val t = list_comb (Const (c, tys ---> ty),
    1.91 -        map Free (Name.names Name.context "a" tys));
    1.92 -      val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify)
    1.93 -        (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
    1.94 -      val cty = Thm.ctyp_of thy ty;
    1.95 -    in
    1.96 -      @{thm term_of_anything}
    1.97 -      |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
    1.98 -      |> Thm.varifyT
    1.99 -    end;
   1.100 -  fun add_term_of_code tyco raw_vs raw_cs thy =
   1.101 -    let
   1.102 -      val algebra = Sign.classes_of thy;
   1.103 -      val vs = map (fn (v, sort) =>
   1.104 -        (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
   1.105 -      val ty = Type (tyco, map TFree vs);
   1.106 -      val cs = (map o apsnd o map o map_atyps)
   1.107 -        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
   1.108 -      val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
   1.109 -      val eqs = map (mk_term_of_eq thy ty vs tyco) cs;
   1.110 -   in
   1.111 -      thy
   1.112 -      |> Code.del_eqns const
   1.113 -      |> fold Code.add_eqn eqs
   1.114 -    end;
   1.115 -  fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
   1.116 -    let
   1.117 -      val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
   1.118 -    in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
   1.119 -in
   1.120 -  Code.type_interpretation ensure_term_of_code
   1.121 -end
   1.122 -*}
   1.123 -
   1.124 -
   1.125 -subsubsection {* Code generator setup *}
   1.126 -
   1.127 -lemmas [code del] = term.recs term.cases term.size
   1.128 -lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
   1.129 -
   1.130 -lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
   1.131 -lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
   1.132 -lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
   1.133 -lemma [code, code del]:
   1.134 -  "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
   1.135 -lemma [code, code del]:
   1.136 -  "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
   1.137 -
   1.138 -lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c =
   1.139 -    (let (n, m) = nibble_pair_of_char c
   1.140 -  in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
   1.141 -    (Code_Eval.term_of n)) (Code_Eval.term_of m))"
   1.142 -  by (subst term_of_anything) rule 
   1.143 -
   1.144 -code_type "term"
   1.145 -  (Eval "Term.term")
   1.146 -
   1.147 -code_const Const and App
   1.148 -  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
   1.149 -
   1.150 -code_const "term_of \<Colon> String.literal \<Rightarrow> term"
   1.151 -  (Eval "HOLogic.mk'_message'_string")
   1.152 -
   1.153 -code_reserved Eval HOLogic
   1.154 -
   1.155 -
   1.156 -subsubsection {* Syntax *}
   1.157 -
   1.158 -definition termify :: "'a \<Rightarrow> term" where
   1.159 -  [code del]: "termify x = dummy_term"
   1.160 -
   1.161 -abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where
   1.162 -  "valtermify x \<equiv> (x, \<lambda>u. termify x)"
   1.163 -
   1.164 -setup {*
   1.165 -let
   1.166 -  fun map_default f xs =
   1.167 -    let val ys = map f xs
   1.168 -    in if exists is_some ys
   1.169 -      then SOME (map2 the_default xs ys)
   1.170 -      else NONE
   1.171 -    end;
   1.172 -  fun subst_termify_app (Const (@{const_name termify}, T), [t]) =
   1.173 -        if not (Term.has_abs t)
   1.174 -        then if fold_aterms (fn Const _ => I | _ => K false) t true
   1.175 -          then SOME (HOLogic.reflect_term t)
   1.176 -          else error "Cannot termify expression containing variables"
   1.177 -        else error "Cannot termify expression containing abstraction"
   1.178 -    | subst_termify_app (t, ts) = case map_default subst_termify ts
   1.179 -       of SOME ts' => SOME (list_comb (t, ts'))
   1.180 -        | NONE => NONE
   1.181 -  and subst_termify (Abs (v, T, t)) = (case subst_termify t
   1.182 -       of SOME t' => SOME (Abs (v, T, t'))
   1.183 -        | NONE => NONE)
   1.184 -    | subst_termify t = subst_termify_app (strip_comb t) 
   1.185 -  fun check_termify ts ctxt = map_default subst_termify ts
   1.186 -    |> Option.map (rpair ctxt)
   1.187 -in
   1.188 -  Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
   1.189 -end;
   1.190 -*}
   1.191 -
   1.192 -locale term_syntax
   1.193 -begin
   1.194 -
   1.195 -notation App (infixl "<\<cdot>>" 70)
   1.196 -  and valapp (infixl "{\<cdot>}" 70)
   1.197 -
   1.198 -end
   1.199 -
   1.200 -interpretation term_syntax .
   1.201 -
   1.202 -no_notation App (infixl "<\<cdot>>" 70)
   1.203 -  and valapp (infixl "{\<cdot>}" 70)
   1.204 -
   1.205 -
   1.206 -subsection {* Numeric types *}
   1.207 -
   1.208 -definition term_of_num :: "'a\<Colon>{semiring_div} \<Rightarrow> 'a\<Colon>{semiring_div} \<Rightarrow> term" where
   1.209 -  "term_of_num two = (\<lambda>_. dummy_term)"
   1.210 -
   1.211 -lemma (in term_syntax) term_of_num_code [code]:
   1.212 -  "term_of_num two k = (if k = 0 then termify Int.Pls
   1.213 -    else (if k mod two = 0
   1.214 -      then termify Int.Bit0 <\<cdot>> term_of_num two (k div two)
   1.215 -      else termify Int.Bit1 <\<cdot>> term_of_num two (k div two)))"
   1.216 -  by (auto simp add: term_of_anything Const_def App_def term_of_num_def Let_def)
   1.217 -
   1.218 -lemma (in term_syntax) term_of_nat_code [code]:
   1.219 -  "term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num (2::nat) n"
   1.220 -  by (simp only: term_of_anything)
   1.221 -
   1.222 -lemma (in term_syntax) term_of_int_code [code]:
   1.223 -  "term_of (k::int) = (if k = 0 then termify (0 :: int)
   1.224 -    else if k > 0 then termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) k
   1.225 -      else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
   1.226 -  by (simp only: term_of_anything)
   1.227 -
   1.228 -lemma (in term_syntax) term_of_code_numeral_code [code]:
   1.229 -  "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
   1.230 -  by (simp only: term_of_anything)
   1.231 -
   1.232 -subsection {* Obfuscate *}
   1.233 -
   1.234 -print_translation {*
   1.235 -let
   1.236 -  val term = Const ("<TERM>", dummyT);
   1.237 -  fun tr1' [_, _] = term;
   1.238 -  fun tr2' [] = term;
   1.239 -in
   1.240 -  [(@{const_syntax Const}, tr1'),
   1.241 -    (@{const_syntax App}, tr1'),
   1.242 -    (@{const_syntax dummy_term}, tr2')]
   1.243 -end
   1.244 -*}
   1.245 -
   1.246 -hide const dummy_term App valapp
   1.247 -hide (open) const Const termify valtermify term_of term_of_num
   1.248 -
   1.249 -
   1.250 -subsection {* Evaluation setup *}
   1.251 -
   1.252 -ML {*
   1.253 -signature EVAL =
   1.254 -sig
   1.255 -  val eval_ref: (unit -> term) option ref
   1.256 -  val eval_term: theory -> term -> term
   1.257 -end;
   1.258 -
   1.259 -structure Eval : EVAL =
   1.260 -struct
   1.261 -
   1.262 -val eval_ref = ref (NONE : (unit -> term) option);
   1.263 -
   1.264 -fun eval_term thy t =
   1.265 -  Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
   1.266 -
   1.267 -end;
   1.268 -*}
   1.269 -
   1.270 -setup {*
   1.271 -  Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of)
   1.272 -*}
   1.273 -
   1.274 -end

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Code_Evaluation.thy	Wed Sep 23 14:00:12 2009 +0200
     2.3 @@ -0,0 +1,271 @@
     2.4 +(*  Title:      HOL/Code_Evaluation.thy
     2.5 +    Author:     Florian Haftmann, TU Muenchen
     2.6 +*)
     2.7 +
     2.8 +header {* Term evaluation using the generic code generator *}
     2.9 +
    2.10 +theory Code_Evaluation
    2.11 +imports Plain Typerep Code_Numeral
    2.12 +begin
    2.13 +
    2.14 +subsection {* Term representation *}
    2.15 +
    2.16 +subsubsection {* Terms and class @{text term_of} *}
    2.17 +
    2.18 +datatype "term" = dummy_term
    2.19 +
    2.20 +definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
    2.21 +  "Const _ _ = dummy_term"
    2.22 +
    2.23 +definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
    2.24 +  "App _ _ = dummy_term"
    2.25 +
    2.26 +code_datatype Const App
    2.27 +
    2.28 +class term_of = typerep +
    2.29 +  fixes term_of :: "'a \<Rightarrow> term"
    2.30 +
    2.31 +lemma term_of_anything: "term_of x \<equiv> t"
    2.32 +  by (rule eq_reflection) (cases "term_of x", cases t, simp)
    2.33 +
    2.34 +definition valapp :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)
    2.35 +  \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
    2.36 +  "valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
    2.37 +
    2.38 +lemma valapp_code [code, code_unfold]:
    2.39 +  "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
    2.40 +  by (simp only: valapp_def fst_conv snd_conv)
    2.41 +
    2.42 +
    2.43 +subsubsection {* @{text term_of} instances *}
    2.44 +
    2.45 +instantiation "fun" :: (typerep, typerep) term_of
    2.46 +begin
    2.47 +
    2.48 +definition
    2.49 +  "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'')
    2.50 +     [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
    2.51 +
    2.52 +instance ..
    2.53 +
    2.54 +end
    2.55 +
    2.56 +setup {*
    2.57 +let
    2.58 +  fun add_term_of tyco raw_vs thy =
    2.59 +    let
    2.60 +      val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
    2.61 +      val ty = Type (tyco, map TFree vs);
    2.62 +      val lhs = Const (@{const_name term_of}, ty --> @{typ term})
    2.63 +        $ Free ("x", ty);
    2.64 +      val rhs = @{term "undefined \<Colon> term"};
    2.65 +      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    2.66 +      fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
    2.67 +        o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
    2.68 +    in
    2.69 +      thy
    2.70 +      |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
    2.71 +      |> `(fn lthy => Syntax.check_term lthy eq)
    2.72 +      |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
    2.73 +      |> snd
    2.74 +      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    2.75 +    end;
    2.76 +  fun ensure_term_of (tyco, (raw_vs, _)) thy =
    2.77 +    let
    2.78 +      val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
    2.79 +        andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
    2.80 +    in if need_inst then add_term_of tyco raw_vs thy else thy end;
    2.81 +in
    2.82 +  Code.type_interpretation ensure_term_of
    2.83 +end
    2.84 +*}
    2.85 +
    2.86 +setup {*
    2.87 +let
    2.88 +  fun mk_term_of_eq thy ty vs tyco (c, tys) =
    2.89 +    let
    2.90 +      val t = list_comb (Const (c, tys ---> ty),
    2.91 +        map Free (Name.names Name.context "a" tys));
    2.92 +      val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify)
    2.93 +        (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
    2.94 +      val cty = Thm.ctyp_of thy ty;
    2.95 +    in
    2.96 +      @{thm term_of_anything}
    2.97 +      |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
    2.98 +      |> Thm.varifyT
    2.99 +    end;
   2.100 +  fun add_term_of_code tyco raw_vs raw_cs thy =
   2.101 +    let
   2.102 +      val algebra = Sign.classes_of thy;
   2.103 +      val vs = map (fn (v, sort) =>
   2.104 +        (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
   2.105 +      val ty = Type (tyco, map TFree vs);
   2.106 +      val cs = (map o apsnd o map o map_atyps)
   2.107 +        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
   2.108 +      val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
   2.109 +      val eqs = map (mk_term_of_eq thy ty vs tyco) cs;
   2.110 +   in
   2.111 +      thy
   2.112 +      |> Code.del_eqns const
   2.113 +      |> fold Code.add_eqn eqs
   2.114 +    end;
   2.115 +  fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
   2.116 +    let
   2.117 +      val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
   2.118 +    in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
   2.119 +in
   2.120 +  Code.type_interpretation ensure_term_of_code
   2.121 +end
   2.122 +*}
   2.123 +
   2.124 +
   2.125 +subsubsection {* Code generator setup *}
   2.126 +
   2.127 +lemmas [code del] = term.recs term.cases term.size
   2.128 +lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
   2.129 +
   2.130 +lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
   2.131 +lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
   2.132 +lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
   2.133 +lemma [code, code del]:
   2.134 +  "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of" ..
   2.135 +lemma [code, code del]:
   2.136 +  "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of" ..
   2.137 +
   2.138 +lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Evaluation.term_of c =
   2.139 +    (let (n, m) = nibble_pair_of_char c
   2.140 +  in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
   2.141 +    (Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))"
   2.142 +  by (subst term_of_anything) rule 
   2.143 +
   2.144 +code_type "term"
   2.145 +  (Eval "Term.term")
   2.146 +
   2.147 +code_const Const and App
   2.148 +  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
   2.149 +
   2.150 +code_const "term_of \<Colon> String.literal \<Rightarrow> term"
   2.151 +  (Eval "HOLogic.mk'_message'_string")
   2.152 +
   2.153 +code_reserved Eval HOLogic
   2.154 +
   2.155 +
   2.156 +subsubsection {* Syntax *}
   2.157 +
   2.158 +definition termify :: "'a \<Rightarrow> term" where
   2.159 +  [code del]: "termify x = dummy_term"
   2.160 +
   2.161 +abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where
   2.162 +  "valtermify x \<equiv> (x, \<lambda>u. termify x)"
   2.163 +
   2.164 +setup {*
   2.165 +let
   2.166 +  fun map_default f xs =
   2.167 +    let val ys = map f xs
   2.168 +    in if exists is_some ys
   2.169 +      then SOME (map2 the_default xs ys)
   2.170 +      else NONE
   2.171 +    end;
   2.172 +  fun subst_termify_app (Const (@{const_name termify}, T), [t]) =
   2.173 +        if not (Term.has_abs t)
   2.174 +        then if fold_aterms (fn Const _ => I | _ => K false) t true
   2.175 +          then SOME (HOLogic.reflect_term t)
   2.176 +          else error "Cannot termify expression containing variables"
   2.177 +        else error "Cannot termify expression containing abstraction"
   2.178 +    | subst_termify_app (t, ts) = case map_default subst_termify ts
   2.179 +       of SOME ts' => SOME (list_comb (t, ts'))
   2.180 +        | NONE => NONE
   2.181 +  and subst_termify (Abs (v, T, t)) = (case subst_termify t
   2.182 +       of SOME t' => SOME (Abs (v, T, t'))
   2.183 +        | NONE => NONE)
   2.184 +    | subst_termify t = subst_termify_app (strip_comb t) 
   2.185 +  fun check_termify ts ctxt = map_default subst_termify ts
   2.186 +    |> Option.map (rpair ctxt)
   2.187 +in
   2.188 +  Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
   2.189 +end;
   2.190 +*}
   2.191 +
   2.192 +locale term_syntax
   2.193 +begin
   2.194 +
   2.195 +notation App (infixl "<\<cdot>>" 70)
   2.196 +  and valapp (infixl "{\<cdot>}" 70)
   2.197 +
   2.198 +end
   2.199 +
   2.200 +interpretation term_syntax .
   2.201 +
   2.202 +no_notation App (infixl "<\<cdot>>" 70)
   2.203 +  and valapp (infixl "{\<cdot>}" 70)
   2.204 +
   2.205 +
   2.206 +subsection {* Numeric types *}
   2.207 +
   2.208 +definition term_of_num :: "'a\<Colon>{semiring_div} \<Rightarrow> 'a\<Colon>{semiring_div} \<Rightarrow> term" where
   2.209 +  "term_of_num two = (\<lambda>_. dummy_term)"
   2.210 +
   2.211 +lemma (in term_syntax) term_of_num_code [code]:
   2.212 +  "term_of_num two k = (if k = 0 then termify Int.Pls
   2.213 +    else (if k mod two = 0
   2.214 +      then termify Int.Bit0 <\<cdot>> term_of_num two (k div two)
   2.215 +      else termify Int.Bit1 <\<cdot>> term_of_num two (k div two)))"
   2.216 +  by (auto simp add: term_of_anything Const_def App_def term_of_num_def Let_def)
   2.217 +
   2.218 +lemma (in term_syntax) term_of_nat_code [code]:
   2.219 +  "term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num (2::nat) n"
   2.220 +  by (simp only: term_of_anything)
   2.221 +
   2.222 +lemma (in term_syntax) term_of_int_code [code]:
   2.223 +  "term_of (k::int) = (if k = 0 then termify (0 :: int)
   2.224 +    else if k > 0 then termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) k
   2.225 +      else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
   2.226 +  by (simp only: term_of_anything)
   2.227 +
   2.228 +lemma (in term_syntax) term_of_code_numeral_code [code]:
   2.229 +  "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
   2.230 +  by (simp only: term_of_anything)
   2.231 +
   2.232 +subsection {* Obfuscate *}
   2.233 +
   2.234 +print_translation {*
   2.235 +let
   2.236 +  val term = Const ("<TERM>", dummyT);
   2.237 +  fun tr1' [_, _] = term;
   2.238 +  fun tr2' [] = term;
   2.239 +in
   2.240 +  [(@{const_syntax Const}, tr1'),
   2.241 +    (@{const_syntax App}, tr1'),
   2.242 +    (@{const_syntax dummy_term}, tr2')]
   2.243 +end
   2.244 +*}
   2.245 +
   2.246 +hide const dummy_term App valapp
   2.247 +hide (open) const Const termify valtermify term_of term_of_num
   2.248 +
   2.249 +
   2.250 +subsection {* Evaluation setup *}
   2.251 +
   2.252 +ML {*
   2.253 +signature EVAL =
   2.254 +sig
   2.255 +  val eval_ref: (unit -> term) option ref
   2.256 +  val eval_term: theory -> term -> term
   2.257 +end;
   2.258 +
   2.259 +structure Eval : EVAL =
   2.260 +struct
   2.261 +
   2.262 +val eval_ref = ref (NONE : (unit -> term) option);
   2.263 +
   2.264 +fun eval_term thy t =
   2.265 +  Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
   2.266 +
   2.267 +end;
   2.268 +*}
   2.269 +
   2.270 +setup {*
   2.271 +  Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of)
   2.272 +*}
   2.273 +
   2.274 +end

     3.1 --- a/src/HOL/IsaMakefile	Wed Sep 23 13:42:53 2009 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Wed Sep 23 14:00:12 2009 +0200
     3.3 @@ -210,7 +210,7 @@
     3.4  
     3.5  MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
     3.6    ATP_Linkup.thy \
     3.7 -  Code_Eval.thy \
     3.8 +  Code_Evaluation.thy \
     3.9    Code_Numeral.thy \
    3.10    Equiv_Relations.thy \
    3.11    Groebner_Basis.thy \

     4.1 --- a/src/HOL/Library/Code_Char.thy	Wed Sep 23 13:42:53 2009 +0200
     4.2 +++ b/src/HOL/Library/Code_Char.thy	Wed Sep 23 14:00:12 2009 +0200
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* Code generation of pretty characters (and strings) *}
     4.5  
     4.6  theory Code_Char
     4.7 -imports List Code_Eval Main
     4.8 +imports List Code_Evaluation Main
     4.9  begin
    4.10  
    4.11  code_type char
    4.12 @@ -32,7 +32,7 @@
    4.13    (OCaml "!((_ : char) = _)")
    4.14    (Haskell infixl 4 "==")
    4.15  
    4.16 -code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term"
    4.17 +code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
    4.18    (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
    4.19  
    4.20  end

     5.1 --- a/src/HOL/Library/Code_Integer.thy	Wed Sep 23 13:42:53 2009 +0200
     5.2 +++ b/src/HOL/Library/Code_Integer.thy	Wed Sep 23 14:00:12 2009 +0200
     5.3 @@ -100,7 +100,7 @@
     5.4  
     5.5  text {* Evaluation *}
     5.6  
     5.7 -code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term"
     5.8 +code_const "Code_Evaluation.term_of \<Colon> int \<Rightarrow> term"
     5.9    (Eval "HOLogic.mk'_number/ HOLogic.intT")
    5.10  
    5.11  end
    5.12 \ No newline at end of file

     6.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Sep 23 13:42:53 2009 +0200
     6.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Wed Sep 23 14:00:12 2009 +0200
     6.3 @@ -415,9 +415,9 @@
     6.4  text {* Evaluation *}
     6.5  
     6.6  lemma [code, code del]:
     6.7 -  "(Code_Eval.term_of \<Colon> nat \<Rightarrow> term) = Code_Eval.term_of" ..
     6.8 +  "(Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term) = Code_Evaluation.term_of" ..
     6.9  
    6.10 -code_const "Code_Eval.term_of \<Colon> nat \<Rightarrow> term"
    6.11 +code_const "Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term"
    6.12    (SML "HOLogic.mk'_number/ HOLogic.natT")
    6.13  
    6.14  

     7.1 --- a/src/HOL/Library/Fin_Fun.thy	Wed Sep 23 13:42:53 2009 +0200
     7.2 +++ b/src/HOL/Library/Fin_Fun.thy	Wed Sep 23 14:00:12 2009 +0200
     7.3 @@ -311,17 +311,17 @@
     7.4  notation scomp (infixl "o\<rightarrow>" 60)
     7.5  
     7.6  definition (in term_syntax) valtermify_finfun_const ::
     7.7 -  "'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a\<Colon>typerep \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term)" where
     7.8 -  "valtermify_finfun_const y = Code_Eval.valtermify finfun_const {\<cdot>} y"
     7.9 +  "'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> ('a\<Colon>typerep \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
    7.10 +  "valtermify_finfun_const y = Code_Evaluation.valtermify finfun_const {\<cdot>} y"
    7.11  
    7.12  definition (in term_syntax) valtermify_finfun_update_code ::
    7.13 -  "'a\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> 'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term)" where
    7.14 -  "valtermify_finfun_update_code x y f = Code_Eval.valtermify finfun_update_code {\<cdot>} f {\<cdot>} x {\<cdot>} y"
    7.15 +  "'a\<Colon>typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> 'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
    7.16 +  "valtermify_finfun_update_code x y f = Code_Evaluation.valtermify finfun_update_code {\<cdot>} f {\<cdot>} x {\<cdot>} y"
    7.17  
    7.18  instantiation finfun :: (random, random) random
    7.19  begin
    7.20  
    7.21 -primrec random_finfun_aux :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
    7.22 +primrec random_finfun_aux :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" where
    7.23      "random_finfun_aux 0 j = Quickcheck.collapse (Random.select_weight
    7.24         [(1, Quickcheck.random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
    7.25    | "random_finfun_aux (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_weight

     8.1 --- a/src/HOL/Library/Nested_Environment.thy	Wed Sep 23 13:42:53 2009 +0200
     8.2 +++ b/src/HOL/Library/Nested_Environment.thy	Wed Sep 23 14:00:12 2009 +0200
     8.3 @@ -567,6 +567,6 @@
     8.4  qed simp_all
     8.5  
     8.6  lemma [code, code del]:
     8.7 -  "(Code_Eval.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Eval.term_of" ..
     8.8 +  "(Code_Evaluation.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Evaluation.term_of" ..
     8.9  
    8.10  end

     9.1 --- a/src/HOL/Quickcheck.thy	Wed Sep 23 13:42:53 2009 +0200
     9.2 +++ b/src/HOL/Quickcheck.thy	Wed Sep 23 14:00:12 2009 +0200
     9.3 @@ -3,7 +3,7 @@
     9.4  header {* A simple counterexample generator *}
     9.5  
     9.6  theory Quickcheck
     9.7 -imports Random Code_Eval
     9.8 +imports Random Code_Evaluation
     9.9  uses ("Tools/quickcheck_generators.ML")
    9.10  begin
    9.11  
    9.12 @@ -24,7 +24,7 @@
    9.13  
    9.14  definition
    9.15    "random i = Random.range 2 o\<rightarrow>
    9.16 -    (\<lambda>k. Pair (if k = 0 then Code_Eval.valtermify False else Code_Eval.valtermify True))"
    9.17 +    (\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))"
    9.18  
    9.19  instance ..
    9.20  
    9.21 @@ -34,7 +34,7 @@
    9.22  begin
    9.23  
    9.24  definition random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
    9.25 -  "random_itself _ = Pair (Code_Eval.valtermify TYPE('a))"
    9.26 +  "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))"
    9.27  
    9.28  instance ..
    9.29  
    9.30 @@ -44,7 +44,7 @@
    9.31  begin
    9.32  
    9.33  definition
    9.34 -  "random _ = Random.select chars o\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Eval.term_of c))"
    9.35 +  "random _ = Random.select chars o\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
    9.36  
    9.37  instance ..
    9.38  
    9.39 @@ -54,7 +54,7 @@
    9.40  begin
    9.41  
    9.42  definition 
    9.43 -  "random _ = Pair (STR '''', \<lambda>u. Code_Eval.term_of (STR ''''))"
    9.44 +  "random _ = Pair (STR '''', \<lambda>u. Code_Evaluation.term_of (STR ''''))"
    9.45  
    9.46  instance ..
    9.47  
    9.48 @@ -63,10 +63,10 @@
    9.49  instantiation nat :: random
    9.50  begin
    9.51  
    9.52 -definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
    9.53 +definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" where
    9.54    "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (
    9.55       let n = Code_Numeral.nat_of k
    9.56 -     in (n, \<lambda>_. Code_Eval.term_of n)))"
    9.57 +     in (n, \<lambda>_. Code_Evaluation.term_of n)))"
    9.58  
    9.59  instance ..
    9.60  
    9.61 @@ -78,7 +78,7 @@
    9.62  definition
    9.63    "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (
    9.64       let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
    9.65 -     in (j, \<lambda>_. Code_Eval.term_of j)))"
    9.66 +     in (j, \<lambda>_. Code_Evaluation.term_of j)))"
    9.67  
    9.68  instance ..
    9.69  
    9.70 @@ -95,7 +95,7 @@
    9.71  
    9.72  definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
    9.73    \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
    9.74 -  "random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of f Random.split_seed"
    9.75 +  "random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
    9.76  
    9.77  instantiation "fun" :: ("{eq, term_of}", random) random
    9.78  begin

    10.1 --- a/src/HOL/Rational.thy	Wed Sep 23 13:42:53 2009 +0200
    10.2 +++ b/src/HOL/Rational.thy	Wed Sep 23 14:00:12 2009 +0200
    10.3 @@ -1002,8 +1002,8 @@
    10.4    by simp
    10.5  
    10.6  definition (in term_syntax)
    10.7 -  valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Eval.term)" where
    10.8 -  [code_unfold]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
    10.9 +  valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
   10.10 +  [code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\<cdot>} k {\<cdot>} l"
   10.11  
   10.12  notation fcomp (infixl "o>" 60)
   10.13  notation scomp (infixl "o\<rightarrow>" 60)
   10.14 @@ -1014,7 +1014,7 @@
   10.15  definition
   10.16    "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
   10.17       let j = Code_Numeral.int_of (denom + 1)
   10.18 -     in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))"
   10.19 +     in valterm_fract num (j, \<lambda>u. Code_Evaluation.term_of j))))"
   10.20  
   10.21  instance ..
   10.22  

    11.1 --- a/src/HOL/RealDef.thy	Wed Sep 23 13:42:53 2009 +0200
    11.2 +++ b/src/HOL/RealDef.thy	Wed Sep 23 14:00:12 2009 +0200
    11.3 @@ -1128,8 +1128,8 @@
    11.4    by (simp add: of_rat_divide)
    11.5  
    11.6  definition (in term_syntax)
    11.7 -  valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
    11.8 -  [code_unfold]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
    11.9 +  valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
   11.10 +  [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k"
   11.11  
   11.12  notation fcomp (infixl "o>" 60)
   11.13  notation scomp (infixl "o\<rightarrow>" 60)

    12.1 --- a/src/HOL/Tools/hologic.ML	Wed Sep 23 13:42:53 2009 +0200
    12.2 +++ b/src/HOL/Tools/hologic.ML	Wed Sep 23 14:00:12 2009 +0200
    12.3 @@ -613,17 +613,17 @@
    12.4    | mk_typerep (T as TFree _) = Const ("Typerep.typerep_class.typerep",
    12.5        Term.itselfT T --> typerepT) $ Logic.mk_type T;
    12.6  
    12.7 -val termT = Type ("Code_Eval.term", []);
    12.8 +val termT = Type ("Code_Evaluation.term", []);
    12.9  
   12.10 -fun term_of_const T = Const ("Code_Eval.term_of_class.term_of", T --> termT);
   12.11 +fun term_of_const T = Const ("Code_Evaluation.term_of_class.term_of", T --> termT);
   12.12  
   12.13  fun mk_term_of T t = term_of_const T $ t;
   12.14  
   12.15  fun reflect_term (Const (c, T)) =
   12.16 -      Const ("Code_Eval.Const", literalT --> typerepT --> termT)
   12.17 +      Const ("Code_Evaluation.Const", literalT --> typerepT --> termT)
   12.18          $ mk_literal c $ mk_typerep T
   12.19    | reflect_term (t1 $ t2) =
   12.20 -      Const ("Code_Eval.App", termT --> termT --> termT)
   12.21 +      Const ("Code_Evaluation.App", termT --> termT --> termT)
   12.22          $ reflect_term t1 $ reflect_term t2
   12.23    | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t)
   12.24    | reflect_term t = t;
   12.25 @@ -631,7 +631,7 @@
   12.26  fun mk_valtermify_app c vs T =
   12.27    let
   12.28      fun termifyT T = mk_prodT (T, unitT --> termT);
   12.29 -    fun valapp T T' = Const ("Code_Eval.valapp",
   12.30 +    fun valapp T T' = Const ("Code_Evaluation.valapp",
   12.31        termifyT (T --> T') --> termifyT T --> termifyT T');
   12.32      fun mk_fTs [] _ = []
   12.33        | mk_fTs (_ :: Ts) T = (Ts ---> T) :: mk_fTs Ts T;

    13.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Wed Sep 23 13:42:53 2009 +0200
    13.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Wed Sep 23 14:00:12 2009 +0200
    13.3 @@ -76,7 +76,7 @@
    13.4      val lhs = HOLogic.mk_random T size;
    13.5      val rhs = HOLogic.mk_ST [((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, Tm'))]
    13.6        (HOLogic.mk_return Tm @{typ Random.seed}
    13.7 -      (mk_const "Code_Eval.valapp" [T', T]
    13.8 +      (mk_const "Code_Evaluation.valapp" [T', T]
    13.9          $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
   13.10        @{typ Random.seed} (SOME Tm, @{typ Random.seed});
   13.11      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));

    14.1 --- a/src/HOL/ex/predicate_compile.ML	Wed Sep 23 13:42:53 2009 +0200
    14.2 +++ b/src/HOL/ex/predicate_compile.ML	Wed Sep 23 14:00:12 2009 +0200
    14.3 @@ -169,7 +169,7 @@
    14.4    end;
    14.5  
    14.6  fun dest_randomT (Type ("fun", [@{typ Random.seed},
    14.7 -  Type ("*", [Type ("*", [T, @{typ "unit => Code_Eval.term"}]) ,@{typ Random.seed}])])) = T
    14.8 +  Type ("*", [Type ("*", [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
    14.9    | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
   14.10  
   14.11  (* destruction of intro rules *)
   14.12 @@ -707,7 +707,7 @@
   14.13  end;
   14.14  
   14.15  (* termify_code:
   14.16 -val termT = Type ("Code_Eval.term", []);
   14.17 +val termT = Type ("Code_Evaluation.term", []);
   14.18  fun termifyT T = HOLogic.mk_prodT (T, HOLogic.unitT --> termT)
   14.19  *)
   14.20  (*
   14.21 @@ -1198,7 +1198,7 @@
   14.22        val t1' = mk_valtermify_term t1
   14.23        val t2' = mk_valtermify_term t2
   14.24      in
   14.25 -      Const ("Code_Eval.valapp", termifyT T --> termifyT T1 --> termifyT T2) $ t1' $ t2'
   14.26 +      Const ("Code_Evaluation.valapp", termifyT T --> termifyT T1 --> termifyT T2) $ t1' $ t2'
   14.27      end
   14.28    | mk_valtermify_term _ = error "Not a valid term for mk_valtermify_term"
   14.29  *)