equal
deleted
inserted
replaced
99 | com_tr (Const ("While",_) $ b $ I $ c) xs = |
99 | com_tr (Const ("While",_) $ b $ I $ c) xs = |
100 Syntax.const "While" $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs |
100 Syntax.const "While" $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs |
101 | com_tr t _ = t (* if t is just a Free/Var *) |
101 | com_tr t _ = t (* if t is just a Free/Var *) |
102 *} |
102 *} |
103 |
103 |
104 (* triple_tr *) |
104 (* triple_tr *) (* FIXME does not handle "_idtdummy" *) |
105 ML{* |
105 ML{* |
106 local |
106 local |
107 |
107 |
108 fun var_tr(Free(a,_)) = (a,Bound 0) (* Bound 0 = dummy term *) |
108 fun var_tr(Free(a,_)) = (a,Bound 0) (* Bound 0 = dummy term *) |
109 | var_tr(Const ("_constrain", _) $ (Free (a,_)) $ T) = (a,T); |
109 | var_tr(Const ("_constrain", _) $ (Free (a,_)) $ T) = (a,T); |