81 "~~~~~ fun stac2tac_, args:"; val (pt, thy, (Const("Script.Check'_elementwise",_) $ _ $ |
81 "~~~~~ fun stac2tac_, args:"; val (pt, thy, (Const("Script.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)*) |
86 if nxt = ("Check_elementwise", Check_elementwise "Assumptions") then () |
86 case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => () |
87 else error "Check_elementwise changed; after switch sub-->root-method"; |
87 | _ => error "Check_elementwise changed; after switch sub-->root-method"; |