# HG changeset patch # User haftmann # Date 1256923961 -3600 # Node ID 4db1b31b246ed22ab7d23ed61f3e31f92af89153 # Parent 2bd12592c5e852da941bbe4a5b13180bbc8b3298 set Pure theory name properly diff -r 2bd12592c5e8 -r 4db1b31b246e src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Fri Oct 30 18:32:40 2009 +0100 +++ b/src/Pure/pure_thy.ML Fri Oct 30 18:32:41 2009 +0100 @@ -268,7 +268,8 @@ (* main content *) val _ = Context.>> (Context.map_theory - (OldApplSyntax.init #> + (Sign.map_naming (Name_Space.set_theory_name Context.PureN) #> + OldApplSyntax.init #> Sign.add_types [(Binding.name "fun", 2, NoSyn), (Binding.name "prop", 0, NoSyn),