equal
deleted
inserted
replaced
110 | mk_Fun(name,v,n) = (name,Fun(v,[],n, fn () => C name)); |
110 | mk_Fun(name,v,n) = (name,Fun(v,[],n, fn () => C name)); |
111 |
111 |
112 |
112 |
113 (* ------------------ evaluation with greetings to Tarski ------------------ *) |
113 (* ------------------ evaluation with greetings to Tarski ------------------ *) |
114 |
114 |
115 fun prep_term thy (Const c) = Const (CodegenNames.const thy (CodegenConsts.norm_of_typ thy c), dummyT) |
115 fun prep_term thy (Const c) = Const (CodegenNames.const thy |
|
116 (CodegenConsts.const_of_cexpr thy c), dummyT) |
116 | prep_term thy (Free v_ty) = Free v_ty |
117 | prep_term thy (Free v_ty) = Free v_ty |
117 | prep_term thy (s $ t) = prep_term thy s $ prep_term thy t |
118 | prep_term thy (s $ t) = prep_term thy s $ prep_term thy t |
118 | prep_term thy (Abs (raw_v, ty, raw_t)) = |
119 | prep_term thy (Abs (raw_v, ty, raw_t)) = |
119 let |
120 let |
120 val (v, t) = Syntax.variant_abs (raw_v, ty, raw_t); |
121 val (v, t) = Syntax.variant_abs (raw_v, ty, raw_t); |