# HG changeset patch
# User wenzelm
# Date 1116773476 -7200
# Node ID a2c790d145ba7841e978741e615191844edcab92
# Parent  77c1171090d966428790c89fc71f02aec4111130
fold ProofContext.declare_term;

diff -r 77c1171090d9 -r a2c790d145ba src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun May 22 16:51:15 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Sun May 22 16:51:16 2005 +0200
@@ -1110,7 +1110,7 @@
        Parameters new in context elements must receive types that are
        distinct from types of parameters in target (fixed_params).  *)
     val ctxt_with_fixed =
-      ProofContext.declare_terms (map Free fixed_params) ctxt;
+      fold ProofContext.declare_term (map Free fixed_params) ctxt;
     val int_elemss =
       raw_elemss
       |> List.mapPartial (fn (id, Int es) => SOME (id, es) | _ => NONE)
@@ -1248,13 +1248,13 @@
     val raw_propps = map List.concat raw_proppss;
     val raw_propp = List.concat raw_propps;
 
-    (* CB: add type information from fixed_params to context (declare_terms) *)
+    (* CB: add type information from fixed_params to context (declare_term) *)
     (* CB: process patterns (conclusion and external elements only) *)
     val (ctxt, all_propp) =
-      prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
+      prepp (fold ProofContext.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
     (* CB: add type information from conclusion and external elements
        to context *)
-    val ctxt = ProofContext.declare_terms (List.concat (map (map fst) all_propp)) ctxt;
+    val ctxt = fold ProofContext.declare_term (List.concat (map (map fst) all_propp)) ctxt;
 
     (* CB: resolve schematic variables (patterns) in conclusion and external
        elements. *)