equal
deleted
inserted
replaced
47 |
47 |
48 val nullT = Type ("Null", []); |
48 val nullT = Type ("Null", []); |
49 val nullt = Const ("Null", nullT); |
49 val nullt = Const ("Null", nullT); |
50 |
50 |
51 fun mk_typ T = |
51 fun mk_typ T = |
52 Const ("Type", itselfT T --> Type ("Type", [])) $ Logic.mk_type T; |
52 Const ("Type", Term.itselfT T --> Type ("Type", [])) $ Logic.mk_type T; |
53 |
53 |
54 fun typeof_proc defaultS vs (Const ("typeof", _) $ u) = |
54 fun typeof_proc defaultS vs (Const ("typeof", _) $ u) = |
55 SOME (mk_typ (case strip_comb u of |
55 SOME (mk_typ (case strip_comb u of |
56 (Var ((a, i), _), _) => |
56 (Var ((a, i), _), _) => |
57 if a mem vs then TFree ("'" ^ a ^ ":" ^ string_of_int i, defaultS) |
57 if a mem vs then TFree ("'" ^ a ^ ":" ^ string_of_int i, defaultS) |