src/Pure/axclass.ML
changeset 36419 7aea10d10113
parent 36418 752ee03427c2
child 36420 66fd989c8e15
     1.1 --- a/src/Pure/axclass.ML	Tue Apr 27 14:41:27 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue Apr 27 15:03:19 2010 +0200
     1.3 @@ -249,7 +249,7 @@
     1.4    |> map_filter (fn ((c', _), (_, name)) => if c = c' then SOME name else NONE)
     1.5    |> rev;
     1.6  
     1.7 -fun insert_arity_completions thy (t, ((c, Ss), ((th, thy_name)))) arities =
     1.8 +fun insert_arity_completions thy t ((c, Ss), ((th, thy_name))) (finished, arities) =
     1.9    let
    1.10      val algebra = Sign.classes_of thy;
    1.11      val ars = Symtab.lookup_list arities t;
    1.12 @@ -263,28 +263,31 @@
    1.13  
    1.14      val completions = super_class_completions |> map (fn c1 =>
    1.15        let
    1.16 -        val th1 = (th RS the_classrel thy (c, c1))
    1.17 +        val th1 =
    1.18 +          (th RS the_classrel thy (c, c1))
    1.19            |> Drule.instantiate' std_vars []
    1.20            |> Thm.close_derivation;
    1.21        in ((th1, thy_name), c1) end);
    1.22 +
    1.23 +    val finished' = finished andalso null completions;
    1.24      val arities' = fold (fn (th, c1) => Symtab.cons_list (t, ((c1, Ss), th))) completions arities;
    1.25 -  in (null completions, arities') end;
    1.26 +  in (finished', arities') end;
    1.27  
    1.28  fun put_arity ((t, Ss, c), th) thy =
    1.29 -  let val arity = (t, ((c, Ss), (th, Context.theory_name thy))) in
    1.30 +  let val ar = ((c, Ss), (th, Context.theory_name thy)) in
    1.31      thy
    1.32      |> map_proven_arities
    1.33 -      (Symtab.insert_list (eq_fst op =) arity #> insert_arity_completions thy arity #> #2)
    1.34 +      (Symtab.insert_list (eq_fst op =) (t, ar) #>
    1.35 +       curry (insert_arity_completions thy t ar) true #> #2)
    1.36    end;
    1.37  
    1.38  fun complete_arities thy =
    1.39    let
    1.40      val arities = proven_arities_of thy;
    1.41 -    val (finished, arities') = arities
    1.42 -      |> fold_map (insert_arity_completions thy) (Symtab.dest_list arities);
    1.43 +    val (finished, arities') =
    1.44 +      Symtab.fold (fn (t, ars) => fold (insert_arity_completions thy t) ars) arities (true, arities);
    1.45    in
    1.46 -    if forall I finished
    1.47 -    then NONE
    1.48 +    if finished then NONE
    1.49      else SOME (map_proven_arities (K arities') thy)
    1.50    end;
    1.51