added Isar/local_defs.ML;

--- a/src/Pure/IsaMakefile	Fri Jul 09 18:48:33 1999 +0200
+++ b/src/Pure/IsaMakefile	Fri Jul 09 18:48:54 1999 +0200
@@ -31,7 +31,7 @@
   Interface/isamode.ML Interface/proof_general.ML Isar/ROOT.ML \
   Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML \
   Isar/comment.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML \
-  Isar/isar_thy.ML Isar/method.ML Isar/outer_lex.ML \
+  Isar/isar_thy.ML Isar/local_defs.ML Isar/method.ML Isar/outer_lex.ML \
   Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML \
   Isar/proof_context.ML Isar/proof_data.ML Isar/proof_history.ML \
   Isar/session.ML Isar/skip_proof.ML Isar/toplevel.ML \

--- a/src/Pure/Isar/ROOT.ML	Fri Jul 09 18:48:33 1999 +0200
+++ b/src/Pure/Isar/ROOT.ML	Fri Jul 09 18:48:54 1999 +0200
@@ -16,6 +16,7 @@
 use "method.ML";
 
 (*derived proof elements*)
+use "local_defs.ML";
 use "calculation.ML";
 use "skip_proof.ML";
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/local_defs.ML	Fri Jul 09 18:48:54 1999 +0200
@@ -0,0 +1,49 @@
+(*  Title:      Pure/Isar/local_defs.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Local definitions.
+*)
+
+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) * (term * term list) -> Proof.state -> Proof.state
+end;
+
+structure LocalDefs: LOCAL_DEFS =
+struct
+
+
+val refl_tac = Tactic.rtac Drule.reflexive_thm;
+
+
+fun gen_def fix prep_term match_binds name atts ((x, raw_T), (raw_rhs, raw_pats)) state =
+  let
+    fun err msg = raise Proof.STATE ("Bad local def: " ^ msg, state);
+
+    val state' = fix [(x, raw_T)] state;
+    val ctxt' = Proof.context_of state';
+
+    val rhs = prep_term ctxt' raw_rhs;
+    val T = Term.fastype_of rhs;
+    val lhs = ProofContext.cert_term ctxt' (Free (x, T));
+    val eq = Logic.mk_equals (lhs, rhs);
+  in
+    if lhs mem Term.add_term_frees (rhs, []) then
+      err "lhs occurs on rhs"
+    else if not (Term.term_tfrees rhs subset Term.typ_tfrees T) then
+      err "extra type variables on rhs"
+    else ();
+    state'
+    |> match_binds [(raw_pats, raw_rhs)]   (*note: raw_rhs prepared twice!*)
+    |> Proof.assm_i (refl_tac, refl_tac) name atts [(eq, ([], []))]
+  end;
+
+val def = gen_def Proof.fix ProofContext.read_term Proof.match_bind;
+val def_i = gen_def Proof.fix_i ProofContext.cert_term Proof.match_bind_i;
+
+
+end;