# HG changeset patch
# User ballarin
# Date 1190134157 -7200
# Node ID 4d1876424529da5ce87b472650a18886cf369d55
# Parent  e758837c0d184d1112bcf71cab7371c409e6368c
New function inst_morphism'.

diff -r e758837c0d18 -r 4d1876424529 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Tue Sep 18 18:46:33 2007 +0200
+++ b/src/Pure/Isar/element.ML	Tue Sep 18 18:49:17 2007 +0200
@@ -64,6 +64,7 @@
   val inst_term: typ Symtab.table * term Symtab.table -> term -> term
   val inst_thm: theory -> typ Symtab.table * term Symtab.table -> thm -> thm
   val inst_morphism: theory -> typ Symtab.table * term Symtab.table -> morphism
+  val inst_morphism': theory -> typ Symtab.table * term Symtab.table -> typ Symtab.table * term Symtab.table -> morphism
   val satisfy_thm: witness list -> thm -> thm
   val satisfy_morphism: witness list -> morphism
   val satisfy_facts: witness list ->
@@ -468,6 +469,16 @@
       fact = map (fn th => inst_thm (Theory.deref thy_ref) envs th)}
   end;
 
+(* separate instantiation for theorems -- cannot have vars *)
+fun inst_morphism' thy envs envs' =
+  let val thy_ref = Theory.check_thy thy in
+    Morphism.morphism
+     {name = I, var = I,
+      typ = instT_type (#1 envs),
+      term = inst_term envs,
+      fact = map (fn th => inst_thm (Theory.deref thy_ref) envs' th)}
+  end;
+
 
 (* satisfy hypotheses *)