diff -r a1d63457a3c9 -r fa3f90cf6d9c src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Tue Aug 10 15:07:39 2010 +0200
+++ b/src/Pure/Isar/generic_target.ML	Tue Aug 10 15:09:39 2010 +0200
@@ -71,21 +71,21 @@
     val U = map Term.fastype_of params ---> T;
 
     (*foundation*)
-    val ((lhs', global_def), lthy3) = foundation
+    val ((lhs', global_def), lthy2) = foundation
       (((b, U), mx'), (b_def, rhs')) (type_params, term_params) lthy;
 
     (*local definition*)
-    val ((lhs, local_def), lthy4) = lthy3
+    val ((lhs, local_def), lthy3) = lthy2
       |> Local_Defs.add_def ((b, NoSyn), lhs');
-    val def = Local_Defs.trans_terms lthy4
+    val def = Local_Defs.trans_terms lthy3
       [(*c == global.c xs*)     local_def,
        (*global.c xs == rhs'*)  global_def,
        (*rhs' == rhs*)          Thm.symmetric rhs_conv];
 
     (*note*)
-    val ([(res_name, [res])], lthy5) = lthy4
+    val ([(res_name, [res])], lthy4) = lthy3
       |> Local_Theory.notes_kind "" [((b_def, atts), [([def], [])])];
-  in ((lhs, (res_name, res)), lthy5) end;
+  in ((lhs, (res_name, res)), lthy4) end;
 
 
 (* notes *)