# HG changeset patch
# User wenzelm
# Date 1213631685 -7200
# Node ID ef7cc91a0d7f8de1dfab342f7bc6ab9d0bee8db5
# Parent  c0103bc7f7eb904b8f1948e09638b8baebcad2ae
atomize: proper context;

diff -r c0103bc7f7eb -r ef7cc91a0d7f src/HOLCF/Tools/domain/domain_library.ML
--- a/src/HOLCF/Tools/domain/domain_library.ML	Mon Jun 16 17:54:43 2008 +0200
+++ b/src/HOLCF/Tools/domain/domain_library.ML	Mon Jun 16 17:54:45 2008 +0200
@@ -24,10 +24,10 @@
 fun upd_second f (x,y,z) = (  x, f y,   z);
 fun upd_third  f (x,y,z) = (  x,   y, f z);
 
-fun atomize thm = let val r_inst = Drule.read_instantiate;
+fun atomize ctxt thm = let val r_inst = RuleInsts.read_instantiate ctxt;
     fun at  thm = case concl_of thm of
       _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
-    | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [("x","?"^s)] spec))
+    | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
     | _				    => [thm];
 in map zero_var_indexes (at thm) end;