1.1 --- a/test/Tools/isac/Specify/calchead.sml	Thu May 07 12:15:37 2020 +0200
     1.2 +++ b/test/Tools/isac/Specify/calchead.sml	Thu May 07 14:11:03 2020 +0200
     1.3 @@ -542,7 +542,7 @@
     1.4  val (thy, (str, (dsc, _)): Model_Pattern.single, ty $ var) = (thy, p, a);
     1.5  val ttt = (dsc $ var);
     1.6  Thm.global_cterm_of thy (dsc $ var);
     1.7 -val ori = ((([1], str, dsc, (*[var]*) I_Model.split_dts' (dsc, var))): O_Model.preori);
     1.8 +val ori = ((([1], str, dsc, (*[var]*) O_Model.split_dts' (dsc, var))): O_Model.preori);
     1.9  
    1.10  "-d2-----------------------------------------------------";
    1.11  pbt = [];  (*false*)
    1.12 @@ -555,7 +555,7 @@
    1.13  val (thy, (str, (dsc, _)):Model_Pattern.single, ty $ var) = (thy, p, a);
    1.14  val ttt = (dsc $ var);
    1.15  Thm.global_cterm_of thy (dsc $ var);
    1.16 -val ori = ((([1], str, dsc, (*[var]*) I_Model.split_dts' (dsc, var))): O_Model.preori);
    1.17 +val ori = ((([1], str, dsc, (*[var]*) O_Model.split_dts' (dsc, var))): O_Model.preori);
    1.18  "-d3-----------------------------------------------------";
    1.19  pbt = [];  (*true, base case*)
    1.20  "-----------------continue step through code match_ags---";
    1.21 @@ -575,7 +575,7 @@
    1.22      (is_copy_named_generating_idstr o free2str) t;
    1.23  "--------------------------------------------------------";
    1.24  is_copy_named_generating p (*true*);
    1.25 -           fun sel (_,_,d,ts) = I_Model.comp_ts (d, ts);
    1.26 +           fun sel (_,_,d,ts) = O_Model.comp_ts (d, ts);
    1.27  	   val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t;
    1.28                 (*"v_v"             OLD: "v_"*)
    1.29  	   val ext = (last_elem o drop_last o Symbol.explode o free2str) t;
    1.30 @@ -814,7 +814,7 @@
    1.31        (*#############################^^^^^^^^^ defined by Isabelle*)
    1.32        (2, [1], "#Find", Const ("Simplify.normalform", _ (*"Real.real \<Rightarrow> Tools.una"*)),
    1.33                              [Free ("N", _ (*"Real.real"*))])],
    1.34 -     _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
    1.35 +     _ ) = O_Model.prep_ori fmz thy ((#ppc o get_pbt) pI);
    1.36  "#undef means: the element with description TERM in fmz did not match ";
    1.37  "with any element of pbl (fetched by pI), because there we have Simplify.Term";
    1.38  "defined in Simplify.thy";
    1.39 @@ -842,7 +842,7 @@
    1.40        (*########################^^^^^^^^^ defined in Simplify.thy*)
    1.41        (2, [1], "#Find", Const ("Simplify.normalform", _ ),
    1.42                              [Free ("N", _ )])],
    1.43 -     _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
    1.44 +     _ ) = O_Model.prep_ori fmz thy ((#ppc o get_pbt) pI);
    1.45  
    1.46  "----- we could have checked the pbl at the very beginning and compare with (internal) fmz:";
    1.47  val [("#Given", (Const ("Simplify.Term", _), Free ("t_t", _))),