74 val i = mk_Free (i, T); |
74 val i = mk_Free (i, T); |
75 val E = Env.upd_env E (i, v); |
75 val E = Env.upd_env E (i, v); |
76 body; (*= Const ("Prog_Tac.Check'_elementwise"*) |
76 body; (*= Const ("Prog_Tac.Check'_elementwise"*) |
77 "~~~~~ fun appy, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v)= |
77 "~~~~~ fun appy, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v)= |
78 (thy, ptp, E, (up@[R,D]), body, a, v); |
78 (thy, ptp, E, (up@[R,D]), body, a, v); |
79 handle_leaf "next " th sr E a v t; (*= (NONE, STac (Const ("Prog_Tac.Check'_elementwise"*) |
79 handle_leaf "next " th sr (E, (a, v)) t; (*= (NONE, STac (Const ("Prog_Tac.Check'_elementwise"*) |
80 val (a', STac stac) = handle_leaf "next " th sr E a v t; |
80 val (a', STac stac) = handle_leaf "next " th sr (E, (a, v)) t; |
81 "~~~~~ fun stac2tac_, args:"; val (pt, thy, (Const("Prog_Tac.Check'_elementwise",_) $ _ $ |
81 "~~~~~ fun stac2tac_, args:"; val (pt, thy, (Const("Prog_Tac.Check'_elementwise",_) $ _ $ |
82 (set as Const ("Set.Collect",_) $ Abs (_,_,pred)))) = (pt, (assoc_thy th), stac); |
82 (set as Const ("Set.Collect",_) $ Abs (_,_,pred)))) = (pt, (assoc_thy th), stac); |
83 (*2011 changed ^^^^^ *) |
83 (*2011 changed ^^^^^ *) |
84 |
84 |
85 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*WAS nxt = ("Empty_Tac", Empty_Tac)*) |
85 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*WAS nxt = ("Empty_Tac", Empty_Tac)*) |