# HG changeset patch
# User haftmann
# Date 1193751576 -3600
# Node ID ff5815d04c233e4b328e5b9c50b6c750c2a963eb
# Parent  3d6abdd10382f60e592e8e54cb44a052a154253c
clarified

diff -r 3d6abdd10382 -r ff5815d04c23 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Oct 30 14:39:35 2007 +0100
+++ b/src/Pure/Isar/theory_target.ML	Tue Oct 30 14:39:36 2007 +0100
@@ -176,9 +176,9 @@
     val legacy_arg = (c', Term.close_schematic_term (Logic.legacy_varify rhs'));
     val arg = (c', Term.close_schematic_term rhs');
     (* FIXME workaround based on educated guess *)
-    val in_class = is_class andalso c' = NameSpace.qualified (Class.class_prefix target) c;
+    val class_global = is_class andalso c' = NameSpace.qualified (Class.class_prefix target) c;
   in
-    not in_class ?
+    not class_global ?
       (Context.mapping_result
         (Sign.add_abbrev PrintMode.internal pos legacy_arg)
         (ProofContext.add_abbrev PrintMode.internal pos arg)