1.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Thu Jun 16 11:59:29 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Thu Jun 16 13:50:35 2011 +0200
     1.3 @@ -215,7 +215,7 @@
     1.4      union (op =) (resolve_fact facts_offset fact_names name)
     1.5    | add_fact ctxt _ _ (Inference (_, _, deps)) =
     1.6      if AList.defined (op =) deps leo2_ext then
     1.7 -      insert (op =) (ext_name ctxt, General (* or Chained... *))
     1.8 +      insert (op =) (ext_name ctxt, Extensionality)
     1.9      else
    1.10        I
    1.11    | add_fact _ _ _ _ = I