| changeset 28739 | bbb5f83ce602 |
| parent 28715 | 238f9966c80e |
| child 28822 | 7ca11ecbc4fb |
--- a/src/Pure/Isar/class.ML Thu Nov 13 14:19:09 2008 +0100 +++ b/src/Pure/Isar/class.ML Thu Nov 13 14:19:10 2008 +0100 @@ -78,7 +78,7 @@ val class_prefix = Logic.const_of_class o Sign.base_name; fun activate_class_morphism thy class inst morphism = - Locale.get_interpret_morph thy (class_prefix class) "" morphism class inst; + Locale.get_interpret_morph thy class (false, class_prefix class) "" morphism class inst; fun prove_class_interpretation class inst consts hyp_facts def_facts thy = let