# HG changeset patch
# User wenzelm
# Date 1191942644 -7200
# Node ID e0a2c154df261f80cee4722fa136fe6e7408aa09
# Parent  cc2e0e8c81af9bba7404e040b8df025cd0be9b9c
removed LocalTheory.defs/target_morphism operations;

diff -r cc2e0e8c81af -r e0a2c154df26 src/Pure/Isar/instance.ML
--- a/src/Pure/Isar/instance.ML	Tue Oct 09 17:10:43 2007 +0200
+++ b/src/Pure/Isar/instance.ML	Tue Oct 09 17:10:44 2007 +0200
@@ -50,12 +50,11 @@
         consts = LocalTheory.consts,
         axioms = LocalTheory.axioms,
         abbrev = LocalTheory.abbrev,
-        defs = LocalTheory.defs,
+        def = LocalTheory.def,
         notes = LocalTheory.notes,
         type_syntax = LocalTheory.type_syntax,
         term_syntax = LocalTheory.term_syntax,
         declaration = LocalTheory.pretty,
-        target_morphism = LocalTheory.target_morphism,
         target_naming = LocalTheory.target_naming,
         reinit = LocalTheory.reinit,
         exit = LocalTheory.exit