diff -r 080b755377c0 -r 7dded80a953f src/HOL/Tools/Function/relation.ML
--- a/src/HOL/Tools/Function/relation.ML	Tue May 04 08:55:43 2010 +0200
+++ b/src/HOL/Tools/Function/relation.ML	Tue May 04 09:25:38 2010 +0200
@@ -14,19 +14,20 @@
 structure Function_Relation : FUNCTION_RELATION =
 struct
 
-fun inst_thm ctxt rel st =
+fun inst_state_tac ctxt rel st =
   let
     val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
     val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
     val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st
-    val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') [])))
-  in
-    Drule.cterm_instantiate [(Rvar, rel')] st'
+  in case Term.add_vars (prop_of st') [] of
+       [v] => 
+         PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st'
+     | _ => Seq.empty
   end
 
 fun relation_tac ctxt rel i =
   TRY (Function_Common.apply_termination_rule ctxt i)
-  THEN PRIMITIVE (inst_thm ctxt rel)
+  THEN inst_state_tac ctxt rel
 
 val setup =
   Method.setup @{binding relation}