src/Pure/Isar/expression.ML

   | declare_elem _ (Notes _) ctxt = ctxt;
 
 
 (** Finish locale elements **)
 
-fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
-      let val x = Binding.name_of binding
-      in (binding, AList.lookup (op =) parms x, mx) end) fixes)
-  | finish_primitive _ _ (Constrains _) = Constrains []
-  | finish_primitive _ close (Assumes asms) = close (Assumes asms)
-  | finish_primitive _ close (Defines defs) = close (Defines defs)
-  | finish_primitive _ _ (Notes facts) = Notes facts;
+fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) =>
+  let val x = Binding.name_of binding
+  in (binding, AList.lookup (op =) parms x, mx) end);
 
 local
 
 fun closeup _ _ false elem = elem
   | closeup ctxt parms true elem =

             let val ((c, _), t') = Local_Defs.cert_def ctxt (close_frees t)
             in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end))
         | e => e)
       end;
 
-fun finish_elem ctxt parms do_close elem =
-  finish_primitive parms (closeup ctxt parms do_close) elem;
+fun finish_elem _ parms _ (Fixes fixes) = Fixes (finish_fixes parms fixes)
+  | finish_elem _ _ _ (Constrains _) = Constrains []
+  | finish_elem ctxt parms do_close (Assumes asms) = closeup ctxt parms do_close (Assumes asms)
+  | finish_elem ctxt parms do_close (Defines defs) = closeup ctxt parms do_close (Defines defs)
+  | finish_elem _ _ _ (Notes facts) = Notes facts;
 
 fun finish_inst ctxt (loc, (prfx, inst)) =
   let
     val thy = Proof_Context.theory_of ctxt;
     val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;

     val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.check_name o #1) fixes)
       | _ => fn ps => ps) (Fixes fors :: elems') [];
     val (Ts, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
     val parms = xs ~~ Ts;  (* params from expression and elements *)
 
-    val Fixes fors' = finish_primitive parms I (Fixes fors);
+    val fors' = finish_fixes parms fors;
     val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors';
     val (deps, elems'') = finish ctxt6 parms do_close insts elems';
 
   in ((fixed, deps, elems'', concl), (parms, ctxt7)) end