equal
deleted
inserted
replaced
31 |
31 |
32 setup {* |
32 setup {* |
33 let |
33 let |
34 val subst_rterm_of = Eval.mk_term |
34 val subst_rterm_of = Eval.mk_term |
35 (fn (v, _) => error ("illegal free variable in term quotation: " ^ quote v)) |
35 (fn (v, _) => error ("illegal free variable in term quotation: " ^ quote v)) |
36 (RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort)))); |
36 (Typerep.mk (fn (v, sort) => Typerep.typerep (TFree (v, sort)))); |
37 fun subst_rterm_of' (Const (@{const_name rterm_of}, _), [t]) = subst_rterm_of t |
37 fun subst_rterm_of' (Const (@{const_name rterm_of}, _), [t]) = subst_rterm_of t |
38 | subst_rterm_of' (Const (@{const_name rterm_of}, _), _) = |
38 | subst_rterm_of' (Const (@{const_name rterm_of}, _), _) = |
39 error ("illegal number of arguments for " ^ quote @{const_name rterm_of}) |
39 error ("illegal number of arguments for " ^ quote @{const_name rterm_of}) |
40 | subst_rterm_of' (t, ts) = list_comb (t, map (subst_rterm_of' o strip_comb) ts); |
40 | subst_rterm_of' (t, ts) = list_comb (t, map (subst_rterm_of' o strip_comb) ts); |
41 fun subst_rterm_of'' t = |
41 fun subst_rterm_of'' t = |