Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified
authorhaftmann
Tue, 30 Oct 2007 14:39:36 +0100
changeset 25240 ff5815d04c23
parent 25239 3d6abdd10382
child 25241 001ab1d3f567
clarified
src/Pure/Isar/theory_target.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle