equal
deleted
inserted
replaced
45 | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts) |
45 | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts) |
46 | unstar_typ T = T |
46 | unstar_typ T = T |
47 |
47 |
48 fun unstar_term consts term = |
48 fun unstar_term consts term = |
49 let |
49 let |
50 fun delete a = exists (fn x => x = a) consts |
50 fun unstar (Const(a,T) $ t) = if (a mem consts) then (unstar t) |
51 fun unstar (Const(a,T) $ t) = if (delete a) then (unstar t) |
|
52 else (Const(a,unstar_typ T) $ unstar t) |
51 else (Const(a,unstar_typ T) $ unstar t) |
53 | unstar (f $ t) = unstar f $ unstar t |
52 | unstar (f $ t) = unstar f $ unstar t |
54 | unstar (Const(a,T)) = Const(a,unstar_typ T) |
53 | unstar (Const(a,T)) = Const(a,unstar_typ T) |
55 | unstar (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar t) |
54 | unstar (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar t) |
56 | unstar t = t |
55 | unstar t = t |