src/HOL/ex/predicate_compile.ML
changeset 32657 5f13912245ff
parent 32351 96f9e6402403
child 32701 5059a733a4b8
     1.1 --- a/src/HOL/ex/predicate_compile.ML	Wed Sep 23 13:42:53 2009 +0200
     1.2 +++ b/src/HOL/ex/predicate_compile.ML	Wed Sep 23 14:00:12 2009 +0200
     1.3 @@ -169,7 +169,7 @@
     1.4    end;
     1.5  
     1.6  fun dest_randomT (Type ("fun", [@{typ Random.seed},
     1.7 -  Type ("*", [Type ("*", [T, @{typ "unit => Code_Eval.term"}]) ,@{typ Random.seed}])])) = T
     1.8 +  Type ("*", [Type ("*", [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
     1.9    | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
    1.10  
    1.11  (* destruction of intro rules *)
    1.12 @@ -707,7 +707,7 @@
    1.13  end;
    1.14  
    1.15  (* termify_code:
    1.16 -val termT = Type ("Code_Eval.term", []);
    1.17 +val termT = Type ("Code_Evaluation.term", []);
    1.18  fun termifyT T = HOLogic.mk_prodT (T, HOLogic.unitT --> termT)
    1.19  *)
    1.20  (*
    1.21 @@ -1198,7 +1198,7 @@
    1.22        val t1' = mk_valtermify_term t1
    1.23        val t2' = mk_valtermify_term t2
    1.24      in
    1.25 -      Const ("Code_Eval.valapp", termifyT T --> termifyT T1 --> termifyT T2) $ t1' $ t2'
    1.26 +      Const ("Code_Evaluation.valapp", termifyT T --> termifyT T1 --> termifyT T2) $ t1' $ t2'
    1.27      end
    1.28    | mk_valtermify_term _ = error "Not a valid term for mk_valtermify_term"
    1.29  *)