src/Pure/axclass.ML
changeset 42389 b2c6033fc7e4
parent 42383 0ae4ad40d7b5
child 43329 84472e198515
     1.1 --- a/src/Pure/axclass.ML	Mon Apr 18 13:52:23 2011 +0200
     1.2 +++ b/src/Pure/axclass.ML	Mon Apr 18 14:05:39 2011 +0200
     1.3 @@ -59,15 +59,12 @@
     1.4  
     1.5  type param = string * class;
     1.6  
     1.7 -fun add_param pp ((x, c): param) params =
     1.8 +fun add_param ctxt ((x, c): param) params =
     1.9    (case AList.lookup (op =) params x of
    1.10      NONE => (x, c) :: params
    1.11    | SOME c' =>
    1.12 -      let val ctxt = Syntax.init_pretty pp in
    1.13 -        error ("Duplicate class parameter " ^ quote x ^
    1.14 -          " for " ^ Syntax.string_of_sort ctxt [c] ^
    1.15 -          (if c = c' then "" else " and " ^ Syntax.string_of_sort ctxt [c']))
    1.16 -      end);
    1.17 +      error ("Duplicate class parameter " ^ quote x ^ " for " ^ Syntax.string_of_sort ctxt [c] ^
    1.18 +        (if c = c' then "" else " and " ^ Syntax.string_of_sort ctxt [c'])));
    1.19  
    1.20  
    1.21  (* setup data *)
    1.22 @@ -107,10 +104,14 @@
    1.23          proven_arities = proven_arities2, inst_params = inst_params2,
    1.24          diff_classrels = diff_classrels2}) =
    1.25      let
    1.26 +      val ctxt = Syntax.init_pretty pp;
    1.27 +
    1.28        val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2);
    1.29        val params' =
    1.30          if null params1 then params2
    1.31 -        else fold_rev (fn p => if member (op =) params1 p then I else add_param pp p) params2 params1;
    1.32 +        else
    1.33 +          fold_rev (fn p => if member (op =) params1 p then I else add_param ctxt p)
    1.34 +            params2 params1;
    1.35  
    1.36        (*transitive closure of classrels and arity completion is done in Theory.at_begin hook*)
    1.37        val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2);
    1.38 @@ -593,7 +594,7 @@
    1.39        |> #2
    1.40        |> Sign.restore_naming facts_thy
    1.41        |> map_axclasses (Symtab.update (class, axclass))
    1.42 -      |> map_params (fold (fn (x, _) => add_param (Context.pretty ctxt) (x, class)) params);
    1.43 +      |> map_params (fold (fn (x, _) => add_param ctxt (x, class)) params);
    1.44  
    1.45    in (class, result_thy) end;
    1.46