removed obsolete fork_mixfix (back to theory_target.ML);
authorwenzelm
Wed Oct 17 13:55:35 2007 +0200 (2007-10-17)
changeset 25066344b9611c150
parent 25065 25696ce6dff1
child 25067 0f19e65ac0b6
removed obsolete fork_mixfix (back to theory_target.ML);
src/Pure/Isar/class.ML
     1.1 --- a/src/Pure/Isar/class.ML	Wed Oct 17 11:53:35 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Oct 17 13:55:35 2007 +0200
     1.3 @@ -7,8 +7,6 @@
     1.4  
     1.5  signature CLASS =
     1.6  sig
     1.7 -  val fork_mixfix: bool -> bool -> mixfix -> (mixfix * mixfix) * mixfix
     1.8 -
     1.9    val axclass_cmd: bstring * xstring list
    1.10      -> ((bstring * Attrib.src list) * string list) list
    1.11      -> theory -> class * theory
    1.12 @@ -57,13 +55,6 @@
    1.13  val classN = "class";
    1.14  val introN = "intro";
    1.15  
    1.16 -fun fork_mixfix false _ mx = ((NoSyn, NoSyn), mx)
    1.17 -  | fork_mixfix true false mx = ((NoSyn, mx), NoSyn)
    1.18 -  | fork_mixfix true true mx = ((mx, NoSyn), NoSyn);
    1.19 -      (*let
    1.20 -        val mx' = Syntax.unlocalize_mixfix mx;
    1.21 -      in if mx' = mx then ((NoSyn, mx), NoSyn) else ((mx', mx), NoSyn) end;*)
    1.22 -
    1.23  fun prove_interpretation tac prfx_atts expr inst =
    1.24    Locale.interpretation_i I prfx_atts expr inst
    1.25    #> Proof.global_terminal_proof
    1.26 @@ -789,7 +780,6 @@
    1.27      val phi = morphism thy' class;
    1.28  
    1.29      val c' = Sign.full_name thy' c;
    1.30 -    val ((mx', _), _) = fork_mixfix true true mx;
    1.31      val rhs' = (map_types Logic.unvarifyT o Morphism.term phi) rhs;
    1.32      val ty' = Term.fastype_of rhs';
    1.33      val def = (c, Logic.mk_equals (Const (c', ty'), rhs'));
    1.34 @@ -797,7 +787,7 @@
    1.35    in
    1.36      thy'
    1.37      |> Sign.hide_consts_i false [c'']
    1.38 -    |> Sign.declare_const [] (c, ty', mx') |> snd
    1.39 +    |> Sign.declare_const [] (c, ty', mx) |> snd
    1.40      |> Sign.parent_path
    1.41      |> Sign.sticky_prefix prfx
    1.42      |> yield_singleton (PureThy.add_defs_i false) (def, [])