# HG changeset patch
# User wenzelm
# Date 1192622135 -7200
# Node ID 344b9611c1505226350451b11425f41761621678
# Parent  25696ce6dff17c3ed419c2ddae4d241128c37b87
removed obsolete fork_mixfix (back to theory_target.ML);

diff -r 25696ce6dff1 -r 344b9611c150 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Oct 17 11:53:35 2007 +0200
+++ b/src/Pure/Isar/class.ML	Wed Oct 17 13:55:35 2007 +0200
@@ -7,8 +7,6 @@
 
 signature CLASS =
 sig
-  val fork_mixfix: bool -> bool -> mixfix -> (mixfix * mixfix) * mixfix
-
   val axclass_cmd: bstring * xstring list
     -> ((bstring * Attrib.src list) * string list) list
     -> theory -> class * theory
@@ -57,13 +55,6 @@
 val classN = "class";
 val introN = "intro";
 
-fun fork_mixfix false _ mx = ((NoSyn, NoSyn), mx)
-  | fork_mixfix true false mx = ((NoSyn, mx), NoSyn)
-  | fork_mixfix true true mx = ((mx, NoSyn), NoSyn);
-      (*let
-        val mx' = Syntax.unlocalize_mixfix mx;
-      in if mx' = mx then ((NoSyn, mx), NoSyn) else ((mx', mx), NoSyn) end;*)
-
 fun prove_interpretation tac prfx_atts expr inst =
   Locale.interpretation_i I prfx_atts expr inst
   #> Proof.global_terminal_proof
@@ -789,7 +780,6 @@
     val phi = morphism thy' class;
 
     val c' = Sign.full_name thy' c;
-    val ((mx', _), _) = fork_mixfix true true mx;
     val rhs' = (map_types Logic.unvarifyT o Morphism.term phi) rhs;
     val ty' = Term.fastype_of rhs';
     val def = (c, Logic.mk_equals (Const (c', ty'), rhs'));
@@ -797,7 +787,7 @@
   in
     thy'
     |> Sign.hide_consts_i false [c'']
-    |> Sign.declare_const [] (c, ty', mx') |> snd
+    |> Sign.declare_const [] (c, ty', mx) |> snd
     |> Sign.parent_path
     |> Sign.sticky_prefix prfx
     |> yield_singleton (PureThy.add_defs_i false) (def, [])