src/Pure/Isar/proof_context.ML

 
 
 
 (** local syntax **)
 
-val fixedN = "\\<^fixed>";
-val structN = "\\<^struct>";
-
-
 (* translation functions *)
-
-fun fixed_tr x = (fixedN ^ x, curry Term.list_comb (Syntax.free x));
 
 fun context_tr' ctxt =
   let
     val (_, structs, mixfixed) = syntax_of ctxt;
 
     fun tr' (t $ u) = tr' t $ tr' u
       | tr' (Abs (x, T, t)) = Abs (x, T, tr' t)
       | tr' (t as Free (x, T)) =
           let val i = Library.find_index_eq x structs + 1 in
-            if i = 0 andalso x mem_string mixfixed then Const (fixedN ^ x, T)
+            if i = 0 andalso member (op =) mixfixed x then Const (Syntax.fixedN ^ x, T)
             else if i = 1 andalso not (! show_structs) then
               Syntax.const "_struct" $ Syntax.const "_indexdefault"
             else t
           end
       | tr' a = a;
   in tr' end;
 
 
 (* add syntax *)
 
-fun mixfix_type mx = replicate (Syntax.mixfix_args mx) TypeInfer.logicT ---> TypeInfer.logicT;
-
 local
 
-fun mixfix x NONE mx = (fixedN ^ x, mixfix_type mx, Syntax.fix_mixfix x mx)
-  | mixfix x (SOME T) mx = (fixedN ^ x, T, Syntax.fix_mixfix x mx);
+fun mixfix x NONE mx = (Syntax.fixedN ^ x, TypeInfer.mixfixT mx, Syntax.fix_mixfix x mx)
+  | mixfix x (SOME T) mx = (Syntax.fixedN ^ x, T, Syntax.fix_mixfix x mx);
 
 fun prep_mixfix (_, _, NONE) = NONE
   | prep_mixfix (x, opt_T, SOME mx) = SOME (mixfix x opt_T mx);
 
 fun prep_mixfix' (_, _, NONE) = NONE

 
     val is_logtype = Sign.is_logtype thy;
     val structs' = structs @ List.mapPartial prep_struct decls;
     val mxs = List.mapPartial prep_mixfix decls;
     val (fixed, mxs_output) = Library.split_list (List.mapPartial prep_mixfix' decls);
-    val trs = map fixed_tr fixed;
 
     val extend =
       Syntax.extend_const_gram is_logtype ("", false) mxs_output
-      #> Syntax.extend_const_gram is_logtype ("", true) mxs
-      #> Syntax.extend_trfuns ([], mk trs, [], []);
+      #> Syntax.extend_const_gram is_logtype ("", true) mxs;
     val syns' = extend_syntax thy extend syns;
   in ((syns', structs', fixed @ mixfixed), asms, binds, thms, cases, defs) end);
 
 fun syn_of' thy ctxt =
   let

 fun map_defaults f = map_context (fn (syntax, asms, binds, thms, cases, defs) =>
   (syntax, asms, binds, thms, cases, f defs));
 
 in
 
-fun declare_term_syntax t ctxt =
-  ctxt
-  |> map_defaults (fn (types, sorts, used, occ) => (ins_types t types, sorts, used, occ))
-  |> map_defaults (fn (types, sorts, used, occ) => (types, ins_sorts t sorts, used, occ))
-  |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, ins_used t used, occ));
+fun declare_term_syntax t =
+  map_defaults (fn (types, sorts, used, occ) => (ins_types t types, sorts, used, occ))
+  #> map_defaults (fn (types, sorts, used, occ) => (types, ins_sorts t sorts, used, occ))
+  #> map_defaults (fn (types, sorts, used, occ) => (types, sorts, ins_used t used, occ));
 
 fun declare_term t ctxt =
   ctxt
   |> declare_term_syntax t
   |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs t occ))

 
 
 (* type and constant names *)
 
 fun read_tyname ctxt c =
-  if c mem_string used_types ctxt then
+  if member (op =) (used_types ctxt) c then
     TFree (c, the_default (Sign.defaultS (theory_of ctxt)) (def_sort ctxt (c, ~1)))
   else Sign.read_tyname (theory_of ctxt) c;
 
 fun read_const ctxt c =
   (case lookup_skolem ctxt c of

 (* generalize type variables *)
 
 fun generalize_tfrees inner outer =
   let
     val extra_fixes = fixed_names_of inner \\ fixed_names_of outer;
-    fun still_fixed (Free (x, _)) = not (x mem_string extra_fixes)
+    fun still_fixed (Free (x, _)) = not (member (op =) extra_fixes x)
       | still_fixed _ = false;
     val occs_inner = type_occs_of inner;
     val occs_outer = type_occs_of outer;
     fun add a gen =
       if Symtab.defined occs_outer a orelse

   in fn tfrees => fold add tfrees [] end;
 
 fun generalize inner outer ts =
   let
     val tfrees = generalize_tfrees inner outer (map #1 (fold Term.add_tfrees ts []));
-    fun gen (x, S) = if x mem_string tfrees then TVar ((x, 0), S) else TFree (x, S);
+    fun gen (x, S) = if member (op =) tfrees x then TVar ((x, 0), S) else TFree (x, S);
   in map (Term.map_term_types (Term.map_type_tfree gen)) ts end;
 
 
 
 (** export theorems **)

     (syntax, (assumes, f fixes), binds, thms, cases, defs));
 
 fun err_dups ctxt xs = raise CONTEXT ("Duplicate variable(s): " ^ commas_quote xs, ctxt);
 
 val declare =
-  fold declare_term_syntax o
-  List.mapPartial (fn (_, NONE) => NONE | (x, SOME T) => SOME (Free (x, T)));
+  List.mapPartial (fn (_, NONE) => NONE | (x, SOME T) => SOME (Free (x, T)))
+  #> fold declare_term_syntax;
 
 fun add_vars xs Ts ctxt =
   let val xs' = Term.variantlist (map Syntax.skolem xs, map #2 (fixes_of ctxt)) in
     ctxt
     |> declare (xs' ~~ Ts)

   in
     (case Library.duplicates xs of [] => () | dups => err_dups ctxt dups);
     ctxt' |> add xs Ts
   end;
 
-fun prep_type (x, NONE, SOME mx) = ([x], SOME (mixfix_type mx))
+fun prep_type (x, NONE, SOME mx) = ([x], SOME (TypeInfer.mixfixT mx))
   | prep_type (x, opt_T, _) = ([x], opt_T);
 
 in
 
 val fix = gen_fix read_vars add_vars;

 (*Note: improper use may result in variable capture / dynamic scoping!*)
 fun bind_skolem ctxt xs =
   let
     val ctxt' = ctxt |> fix_i [(xs, NONE)];
     fun bind (t as Free (x, T)) =
-          if x mem_string xs then
+          if member (op =) xs x then
             (case lookup_skolem ctxt' x of SOME x' => Free (x', T) | NONE => t)
           else t
       | bind (t $ u) = bind t $ bind u
       | bind (Abs (x, T, t)) = Abs (x, T, bind t)
       | bind a = a;

   let
     fun err msg = raise CONTEXT (msg ^
       "\nThe error(s) above occurred in local definition: " ^ string_of_term ctxt eq, ctxt);
     val (lhs, rhs) = Logic.dest_equals (Term.strip_all_body eq)
       handle TERM _ => err "Not a meta-equality (==)";
-    val (f, xs) = Term.strip_comb lhs;
+    val (f, xs) = Term.strip_comb (Pattern.beta_eta_contract lhs);
     val (c, _) = Term.dest_Free f handle TERM _ =>
       err "Head of lhs must be a free/fixed variable";
 
     fun is_free (Free (x, _)) = not (is_fixed ctxt x)
       | is_free _ = false;

 
     (*fixes*)
     fun prt_fix (x, x') =
       if x = x' then Pretty.str x
       else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')];
-    val fixes = rev (filter_out
-      ((can Syntax.dest_internal o #1) orf (fn (_, x') => x' mem_string structs)) (fixes_of ctxt));
+    val fixes =
+      rev (filter_out ((can Syntax.dest_internal orf member (op =) structs) o #1) (fixes_of ctxt));
     val prt_fixes = if null fixes then []
       else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
         Pretty.commas (map prt_fix fixes))];
 
     (*prems*)