# HG changeset patch
# User wenzelm
# Date 964954402 -7200
# Node ID 52fb37876254bdde8b6aa6a51cd73fc7a192d96f
# Parent  e9f5768bb656a67398ba3881fae510991fdcbb5d
local_def(_i): no constraint on var;
exporter setup;

diff -r e9f5768bb656 -r 52fb37876254 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sun Jul 30 12:52:46 2000 +0200
+++ b/src/Pure/Isar/local_defs.ML	Sun Jul 30 12:53:22 2000 +0200
@@ -8,18 +8,45 @@
 
 signature LOCAL_DEFS =
 sig
-  val def: string -> Proof.context attribute list
-    -> (string * string option) *  (string * string list) -> Proof.state -> Proof.state
-  val def_i: string -> Proof.context attribute list
-    -> (string * typ option) * (term * term list) -> Proof.state -> Proof.state
+  val def: string -> Proof.context attribute list -> string *  (string * string list)
+    -> Proof.state -> Proof.state
+  val def_i: string -> Proof.context attribute list -> string * (term * term list)
+    -> Proof.state -> Proof.state
 end;
 
 structure LocalDefs: LOCAL_DEFS =
 struct
 
+
+(* export_defs *)
+
+local
+
 val refl_tac = Tactic.rtac (Drule.standard (Drule.reflexive_thm RS Drule.triv_goal));
 
-fun gen_def fix prep_term prep_pats raw_name atts ((x, raw_T), (raw_rhs, raw_pats)) state =
+fun dest_lhs cprop =
+  let val x = #1 (Logic.dest_equals (Logic.dest_goal (Thm.term_of cprop)))
+  in Term.dest_Free x; Thm.cterm_of (Thm.sign_of_cterm cprop) x end
+  handle TERM _ => raise TERM ("Malformed definitional assumption encountered:\n" ^
+      quote (Display.string_of_cterm cprop), []);
+
+fun disch_defs cprops thm =
+  thm
+  |> Drule.implies_intr_list cprops
+  |> Drule.forall_intr_list (map dest_lhs cprops)
+  |> Drule.forall_elim_vars 0
+  |> RANGE (replicate (length cprops) refl_tac) 1;
+
+in
+
+val export_defs = (disch_defs, fn _ => fn _ => []);
+
+end;
+
+
+(* def(_i) *)
+
+fun gen_def fix prep_term prep_pats raw_name atts (x, (raw_rhs, raw_pats)) state =
   let
     val _ = Proof.assert_forward state;
     val ctxt = Proof.context_of state;
@@ -34,9 +61,9 @@
     val lhs = ProofContext.bind_skolem ctxt [x] (Free (x, T));
   in
     state
-    |> fix [([x], raw_T)]
+    |> fix [([x], None)]
     |> Proof.match_bind_i [(pats, rhs)]
-    |> Proof.assm_i (refl_tac, refl_tac) [(name, atts, [(Logic.mk_equals (lhs, rhs), ([], []))])]
+    |> Proof.assm_i export_defs [(name, atts, [(Logic.mk_equals (lhs, rhs), ([], []))])]
   end;
 
 val def = gen_def Proof.fix ProofContext.read_term ProofContext.read_term_pats;