src/HOL/BNF/Tools/bnf_def.ML

--- a/src/HOL/BNF/Tools/bnf_def.ML	Wed May 08 06:14:11 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed May 08 09:39:30 2013 +0200
@@ -1075,7 +1075,7 @@
             val goal =
               fold_rev Logic.all (x :: y :: Rs) (mk_Trueprop_eq (lhs, rhs));
           in
-            Goal.prove_sorry lthy [] [] goal (mk_in_rel_tac rel_OO_Grps)
+            Goal.prove_sorry lthy [] [] goal (mk_in_rel_tac (the_single rel_OO_Grps))
             |> Thm.close_derivation
           end;