src/Pure/Isar/element.ML
changeset 18669 cd6d6baf0411
parent 18606 46e7fc90fde3
child 18894 9c8c60853966
     1.1 --- a/src/Pure/Isar/element.ML	Fri Jan 13 01:13:06 2006 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Fri Jan 13 01:13:08 2006 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  signature ELEMENT =
     1.5  sig
     1.6    datatype ('typ, 'term, 'fact) ctxt =
     1.7 -    Fixes of (string * 'typ option * mixfix option) list |
     1.8 +    Fixes of (string * 'typ option * mixfix) list |
     1.9      Constrains of (string * 'typ) list |
    1.10      Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
    1.11      Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
    1.12 @@ -16,14 +16,13 @@
    1.13    type context (*= (string, string, thmref) ctxt*)
    1.14    type context_i (*= (typ, term, thm list) ctxt*)
    1.15    val map_ctxt: {name: string -> string,
    1.16 -    var: string * mixfix option -> string * mixfix option,
    1.17 +    var: string * mixfix -> string * mixfix,
    1.18      typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
    1.19      attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
    1.20    val map_ctxt_values: (typ -> typ) -> (term -> term) -> (thm -> thm) -> context_i -> context_i
    1.21    val pretty_ctxt: ProofContext.context -> context_i -> Pretty.T list
    1.22    val rename: (string * (string * mixfix option)) list -> string -> string
    1.23 -  val rename_var: (string * (string * mixfix option)) list ->
    1.24 -   string * mixfix option -> string * mixfix option
    1.25 +  val rename_var: (string * (string * mixfix option)) list -> string * mixfix -> string * mixfix
    1.26    val rename_term: (string * (string * mixfix option)) list -> term -> term
    1.27    val rename_thm: (string * (string * mixfix option)) list -> thm -> thm
    1.28    val rename_ctxt: (string * (string * mixfix option)) list -> context_i -> context_i
    1.29 @@ -44,7 +43,7 @@
    1.30  (* datatype ctxt *)
    1.31  
    1.32  datatype ('typ, 'term, 'fact) ctxt =
    1.33 -  Fixes of (string * 'typ option * mixfix option) list |
    1.34 +  Fixes of (string * 'typ option * mixfix) list |
    1.35    Constrains of (string * 'typ) list |
    1.36    Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
    1.37    Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
    1.38 @@ -56,8 +55,7 @@
    1.39  fun map_ctxt {name, var, typ, term, fact, attrib} =
    1.40    fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
    1.41         let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
    1.42 -   | Constrains xs => Constrains (xs |> map (fn (x, T) =>
    1.43 -       (#1 (var (x, SOME Syntax.NoSyn)), typ T)))
    1.44 +   | Constrains xs => Constrains (xs |> map (fn (x, T) => (#1 (var (x, NoSyn)), typ T)))
    1.45     | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
    1.46        ((name a, map attrib atts), propps |> map (fn (t, (ps, qs)) =>
    1.47          (term t, (map term ps, map term qs))))))
    1.48 @@ -80,13 +78,13 @@
    1.49      val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
    1.50      val prt_atts = Args.pretty_attribs ctxt;
    1.51  
    1.52 -    fun prt_syn syn =
    1.53 -      let val s = (case syn of NONE => "(structure)" | SOME mx => Syntax.string_of_mixfix mx)
    1.54 +    fun prt_mixfix mx =
    1.55 +      let val s = Syntax.string_of_mixfix mx
    1.56        in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end;
    1.57 -    fun prt_fix (x, SOME T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
    1.58 -          prt_typ T :: Pretty.brk 1 :: prt_syn syn)
    1.59 -      | prt_fix (x, NONE, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn);
    1.60 -    fun prt_constrain (x, T) = prt_fix (x, SOME T, SOME (Syntax.NoSyn));
    1.61 +    fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
    1.62 +          prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
    1.63 +      | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_mixfix mx);
    1.64 +    fun prt_constrain (x, T) = prt_fix (x, SOME T, NoSyn);
    1.65  
    1.66      fun prt_name name = Pretty.str (ProofContext.extern_thm ctxt name);
    1.67      fun prt_name_atts (name, atts) sep =
    1.68 @@ -156,13 +154,13 @@
    1.69    | SOME (x', _) => x');
    1.70  
    1.71  fun rename_var ren (x, mx) =
    1.72 -  (case (AList.lookup (op =) ren (x: string), is_some mx) of
    1.73 +  (case (AList.lookup (op =) ren (x: string), mx) of
    1.74      (NONE, _) => (x, mx)
    1.75 -  | (SOME (x', NONE), true) => (x', SOME Syntax.NoSyn)
    1.76 -  | (SOME (x', NONE), false) => (x', mx)
    1.77 -  | (SOME (x', SOME mx'), true) => (x', SOME mx')
    1.78 -  | (SOME (x', SOME _), false) =>
    1.79 -      error ("Attempt to change syntax of structure parameter " ^ quote x));
    1.80 +  | (SOME (x', NONE), Structure) => (x', mx)
    1.81 +  | (SOME (x', SOME _), Structure) =>
    1.82 +      error ("Attempt to change syntax of structure parameter " ^ quote x)
    1.83 +  | (SOME (x', NONE), _) => (x', NoSyn)
    1.84 +  | (SOME (x', SOME mx'), _) => (x', mx'));
    1.85  
    1.86  fun rename_term ren (Free (x, T)) = Free (rename ren x, T)
    1.87    | rename_term ren (t $ u) = rename_term ren t $ rename_term ren u