1.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml	Tue Aug 31 16:00:13 2010 +0200
     1.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml	Tue Aug 31 16:38:22 2010 +0200
     1.3 @@ -212,12 +212,12 @@
     1.4  
     1.5  val it = () : unit
     1.6  *** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_assoc"]
     1.7 -*** insert: preserved ["Isabelle","RealDef","Theorems","real_add_assoc"]
     1.8 +*** insert: preserved ["Isabelle","RealDef","Theorems","add_assoc"]
     1.9  *** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_minus1"]
    1.10  *** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_2"]
    1.11  *** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_assoc"]
    1.12  *** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_minus_eq1"]
    1.13 -*** insert: preserved ["Isabelle","RealDef","Theorems","real_add_assoc"]
    1.14 +*** insert: preserved ["Isabelle","RealDef","Theorems","add_assoc"]
    1.15  *** insert: preserved ["Isabelle","RealDef","Theorems","real_minus_divide_eq"]
    1.16  *** insert: preserved ["IsacScripts","ListG","Theorems","induct"]
    1.17  *** insert: preserved ["IsacScripts","ListG","Theorems","simps_1"]
    1.18 @@ -233,8 +233,8 @@
    1.19  ----------------------------------
    1.20  
    1.21  val it = () : unit
    1.22 -*** insert: not found ["Isabelle","NatDef","Theorems","le_refl"]
    1.23 -*** insert: not found ["Isabelle","NatDef","Theorems","le_refl"]*)
    1.24 +*** insert: not found ["Isabelle","NatDef","Theorems","real_le_refl"]
    1.25 +*** insert: not found ["Isabelle","NatDef","Theorems","real_le_refl"]*)
    1.26  
    1.27  "----------- ### thes2file ... Exception- Match raised -----------";
    1.28  "----------- ### thes2file ... Exception- Match raised -----------";