# HG changeset patch
# User huffman
# Date 1289306866 28800
# Node ID c67253b83dc8e2464d8e0566c2bb748269f7bc8b
# Parent  1320a07479740f1d58fb37d22433ca9bb3388cbc
avoid using stale theory

diff -r 1320a0747974 -r c67253b83dc8 src/HOLCF/Tools/Domain/domain_induction.ML
--- a/src/HOLCF/Tools/Domain/domain_induction.ML	Mon Nov 08 15:13:45 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_induction.ML	Tue Nov 09 04:47:46 2010 -0800
@@ -50,7 +50,7 @@
     fun is_ID (Const (c, _)) = (c = @{const_name ID})
       | is_ID _              = false;
   in
-    fun map_of_arg v T =
+    fun map_of_arg thy v T =
       let val m = Domain_Take_Proofs.map_of_typ thy subs T;
       in if is_ID m then v else mk_capply (m, v) end;
   end
@@ -66,7 +66,7 @@
           val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts);
           val vs = map Free (ns ~~ Ts);
           val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs));
-          val rhs = list_ccomb (con_const, map2 map_of_arg vs Ts);
+          val rhs = list_ccomb (con_const, map2 (map_of_arg thy) vs Ts);
           val goal = mk_trp (mk_eq (lhs, rhs));
           val rules =
               [abs_inverse] @ con_betas @ @{thms take_con_rules}