# HG changeset patch
# User wenzelm
# Date 1415562568 -3600
# Node ID 4bee6d8c15004624578a572a2201c35f2bef3c1e
# Parent  1f195ed9994126474d40897e1f2cd5edb26248c5
proper context for typedef;

diff -r 1f195ed99941 -r 4bee6d8c1500 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Sun Nov 09 20:41:53 2014 +0100
+++ b/src/HOL/Import/import_rule.ML	Sun Nov 09 20:49:28 2014 +0100
@@ -222,7 +222,7 @@
     val tnames = sort_strings (map fst tfrees)
     val ((_, typedef_info), thy') =
      Typedef.add_typedef_global false (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
-       (SOME (Binding.name rep_name, Binding.name abs_name)) (rtac th2 1) thy
+       (SOME (Binding.name rep_name, Binding.name abs_name)) (fn _ => rtac th2 1) thy
     val aty = #abs_type (#1 typedef_info)
     val th = freezeT (#type_definition (#2 typedef_info))
     val (th_s, _) = Thm.dest_comb (Thm.dest_arg (cprop_of th))