# HG changeset patch
# User wenzelm
# Date 1320515920 -3600
# Node ID 2cb00d068e3b435ebe17fabede1de4cdc26466a4
# Parent  e209da839ff4d1005f6fc2d392286742203d381e
pruned signature;

diff -r e209da839ff4 -r 2cb00d068e3b src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Nov 05 15:00:49 2011 +0100
+++ b/src/Pure/Isar/element.ML	Sat Nov 05 18:58:40 2011 +0100
@@ -46,18 +46,9 @@
   val transform_witness: morphism -> witness -> witness
   val conclude_witness: witness -> thm
   val pretty_witness: Proof.context -> witness -> Pretty.T
-  val instT_type: typ Symtab.table -> typ -> typ
-  val instT_term: typ Symtab.table -> term -> term
-  val instT_thm: theory -> typ Symtab.table -> thm -> thm
   val instT_morphism: theory -> typ Symtab.table -> morphism
-  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 satisfy_thm: witness list -> thm -> thm
   val satisfy_morphism: witness list -> morphism
-  val satisfy_facts: witness list ->
-    (Attrib.binding * (thm list * Attrib.src list) list) list ->
-    (Attrib.binding * (thm list * Attrib.src list) list) list
   val eq_morphism: theory -> thm list -> morphism option
   val transfer_morphism: theory -> morphism
   val generic_note_thmss: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
@@ -461,7 +452,6 @@
     | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm));
 
 val satisfy_morphism = Morphism.thm_morphism o satisfy_thm;
-val satisfy_facts = facts_map o transform_ctxt o satisfy_morphism;
 
 
 (* rewriting with equalities *)