22 fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x; |
22 fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x; |
23 fun upd_first f (x,y,z) = (f x, y, z); |
23 fun upd_first f (x,y,z) = (f x, y, z); |
24 fun upd_second f (x,y,z) = ( x, f y, z); |
24 fun upd_second f (x,y,z) = ( x, f y, z); |
25 fun upd_third f (x,y,z) = ( x, y, f z); |
25 fun upd_third f (x,y,z) = ( x, y, f z); |
26 |
26 |
27 fun atomize thm = let val r_inst = Drule.read_instantiate; |
27 fun atomize ctxt thm = let val r_inst = RuleInsts.read_instantiate ctxt; |
28 fun at thm = case concl_of thm of |
28 fun at thm = case concl_of thm of |
29 _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) |
29 _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) |
30 | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [("x","?"^s)] spec)) |
30 | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec)) |
31 | _ => [thm]; |
31 | _ => [thm]; |
32 in map zero_var_indexes (at thm) end; |
32 in map zero_var_indexes (at thm) end; |
33 |
33 |
34 (* ----- specific support for domain ---------------------------------------- *) |
34 (* ----- specific support for domain ---------------------------------------- *) |
35 |
35 |