# HG changeset patch
# User wenzelm
# Date 1180800333 -7200
# Node ID c75e5ace1c53aa8891aa5c0b8566ab00097f861f
# Parent  a5026e73cfcf374413b2bd9865e3b71321d4d78b
moved specific target/local_abbrev to theory_target.ML;

diff -r a5026e73cfcf -r c75e5ace1c53 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Jun 02 15:28:38 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Jun 02 18:05:33 2007 +0200
@@ -153,9 +153,6 @@
     Context.generic -> Context.generic
   val set_expand_abbrevs: bool -> Proof.context -> Proof.context
   val add_abbrev: string -> bstring * term -> Proof.context -> (term * term) * Proof.context
-  val target_abbrev: Syntax.mode -> (string * mixfix) * term -> morphism ->
-    Context.generic -> Context.generic
-  val local_abbrev: string * term -> Proof.context -> (term * term) * Proof.context
   val verbose: bool ref
   val setmp_verbose: ('a -> 'b) -> 'a -> 'b
   val print_syntax: Proof.context -> unit
@@ -937,30 +934,6 @@
     |> pair (lhs, rhs)
   end;
 
-fun target_abbrev prmode ((c, mx), rhs) phi =
-  let
-    val c' = Morphism.name phi c;
-    val rhs' = Morphism.term phi rhs;
-    val arg' = (c', rhs');
-  in
-    Context.mapping_result
-      (Sign.add_abbrev Syntax.internalM arg') (add_abbrev Syntax.internalM arg')
-    #-> (fn (lhs, _) =>
-      Term.equiv_types (rhs, rhs') ? Morphism.form (target_notation prmode [(lhs, mx)]))
-  end;
-
-fun local_abbrev (x, rhs) =
-  Variable.add_fixes [x] #-> (fn [x'] =>
-    let
-      val T = Term.fastype_of rhs;
-      val lhs = Free (x', T);
-    in
-      Variable.declare_term lhs #>
-      Variable.declare_term rhs #>
-      Assumption.add_assms (K (K (I, Envir.expand_term_frees [((x', T), rhs)]))) [] #> snd #>
-      pair (lhs, rhs)
-    end);
-
 
 (* fixes *)