1.1 --- a/test/Tools/isac/ProgLang/termC.sml	Thu Nov 21 17:31:20 2013 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/termC.sml	Thu Nov 21 18:12:17 2013 +0100
     1.3 @@ -56,22 +56,22 @@
     1.4             (Const ("Int.Bit1...", "Int.int \<Rightarrow> Int.int") $ Const (...)))))*)
     1.5  (*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)
     1.6  @{term "0::real"};
     1.7 -(*Const ("Groups.zero_class.zero", "RealDef.real")*)
     1.8 +(*Const ("Groups.zero_class.zero", "Real.real")*)
     1.9  @{term "1::real"};
    1.10  (**)
    1.11  @{term "5::real"};
    1.12 -(*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> RealDef.real") $
    1.13 +(*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> "Real.real") $
    1.14       (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
    1.15         (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $
    1.16           (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)
    1.17  @{term "-5::real"};
    1.18 -(*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> RealDef.real") $
    1.19 +(*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> "Real.real") $
    1.20       (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
    1.21         (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
    1.22           (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)
    1.23  @{term "- 5::real"};
    1.24 -(*Const ("Groups.uminus_class.uminus", "RealDef.real \<Rightarrow> RealDef.real") $
    1.25 -     (Const ("Int.number_class.number_of", "Int.int \<Rightarrow> RealDef.real") $
    1.26 +(*Const ("Groups.uminus_class.uminus", "Real.real \<Rightarrow> "Real.real") $
    1.27 +     (Const ("Int.number_class.number_of", "Int.int \<Rightarrow> "Real.real") $
    1.28         (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
    1.29           (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $
    1.30             (Const ("Int.Bit1...", "Int.int \<Rightarrow> Int.int") $ Const (...)))))*)
    1.31 @@ -225,9 +225,9 @@
    1.32  print_depth 3; (*999*) insts; 
    1.33   (*val insts =
    1.34     ({}, 
    1.35 -    {(("a", 0), ("RealDef.real", Free ("3", "RealDef.real"))), 
    1.36 -     (("b", 0), ("RealDef.real", Free ("x", "RealDef.real"))),
    1.37 -     (("c", 0), ("RealDef.real", Free ("1", "RealDef.real")))})*)
    1.38 +    {(("a", 0), ("Real.real", Free ("3", "Real.real"))), 
    1.39 +     (("b", 0), ("Real.real", Free ("x", "Real.real"))),
    1.40 +     (("c", 0), ("Real.real", Free ("1", "Real.real")))})*)
    1.41  
    1.42   "----- throws exn MATCH...";
    1.43  (* val t = str2term "x";
    1.44 @@ -407,7 +407,7 @@
    1.45                      |> numbers_to_string;
    1.46   val Var (("a", 0), ty) = t;
    1.47   val Type (str, tys) = ty;
    1.48 - if str = "RealDef.real" andalso tys = [] andalso ty = HOLogic.realT
    1.49 + if str = "Real.real" andalso tys = [] andalso ty = HOLogic.realT
    1.50     then ()
    1.51     else error "termC.sml type-structure of \"?a :: real\" changed";
    1.52