# HG changeset patch
# User haftmann
# Date 1232226449 -3600
# Node ID 4be5e49c74b1c887a4d5000ac72cc0360128679d
# Parent  bc50244cd1d798a27ab6241c552e7392dea1452a
tuned signature

diff -r bc50244cd1d7 -r 4be5e49c74b1 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Sat Jan 17 22:07:15 2009 +0100
+++ b/src/Pure/Isar/class_target.ML	Sat Jan 17 22:07:29 2009 +0100
@@ -115,7 +115,7 @@
   consts: (string * string) list
     (*locale parameter ~> constant name*),
   base_sort: sort,
-  base_morph: Morphism.morphism
+  base_morph: morphism
     (*static part of canonical morphism*),
   assm_intro: thm option,
   of_class: thm,