diff -r a3f565b8ba76 -r 9c94e6a30d29 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Mon Jun 01 13:32:36 2015 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Mon Jun 01 13:35:16 2015 +0200
@@ -112,11 +112,10 @@
       | eta b t = t
   in eta false end;
 
-fun eta_contract_thm p =
+fun eta_contract_thm ctxt p =
   Conv.fconv_rule (Conv.then_conv (Thm.beta_conversion true, fn ct =>
     Thm.transitive (Thm.eta_conversion ct)
-      (Thm.symmetric (Thm.eta_conversion
-        (Thm.global_cterm_of (Thm.theory_of_cterm ct) (eta_contract p (Thm.term_of ct)))))));
+      (Thm.symmetric (Thm.eta_conversion (Thm.cterm_of ctxt (eta_contract p (Thm.term_of ct)))))));
 
 
 (***********************************************************)
@@ -238,7 +237,7 @@
   in
     Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm split_conv}]
       addsimprocs [@{simproc Collect_mem}]) thm'' |>
-        zero_var_indexes |> eta_contract_thm (equal p)
+        zero_var_indexes |> eta_contract_thm ctxt (equal p)
   end;
 
 
@@ -342,7 +341,7 @@
     Thm.instantiate ([], insts) |>
     Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimprocs
       [to_pred_simproc (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps)]) |>
-    eta_contract_thm (is_pred pred_arities) |>
+    eta_contract_thm ctxt (is_pred pred_arities) |>
     Rule_Cases.save thm
   end;
 
@@ -402,7 +401,7 @@
         thm |>
         Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimprocs
           [to_pred_simproc (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps)]) |>
-        eta_contract_thm (is_pred pred_arities)
+        eta_contract_thm ctxt (is_pred pred_arities)
       else thm
   in map preproc end;