1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Tue Jan 11 15:28:03 2011 +0100
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Mon Feb 21 19:40:36 2011 +0100
     1.3 @@ -850,17 +850,17 @@
     1.4  (*.can this formal argument (of a model-pattern) be omitted in the arg-list
     1.5     of a SubProblem ? see ME/ptyps.sml 'type met '.*)
     1.6  fun is_copy_named_idstr str =
     1.7 -    case (rev o explode) str of
     1.8 -	"'":: _ ::"'"::_ => (tracing ((strs2str o (rev o explode)) 
     1.9 +    case (rev o Symbol.explode) str of
    1.10 +	"'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode)) 
    1.11                                    "is_copy_named_idstr: " ^ str ^ " T"); true)
    1.12 -      | _ => (tracing ((strs2str o (rev o explode)) 
    1.13 +      | _ => (tracing ((strs2str o (rev o Symbol.explode)) 
    1.14                                    "is_copy_named_idstr: " ^ str ^ " F"); false);
    1.15  fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t;
    1.16  
    1.17  (*.should this formal argument (of a model-pattern) create a new identifier?.*)
    1.18  fun is_copy_named_generating_idstr str =
    1.19      if is_copy_named_idstr str
    1.20 -    then case (rev o explode) str of
    1.21 +    then case (rev o Symbol.explode) str of
    1.22  	"'"::"'"::"'"::_ => false
    1.23        | _ => true
    1.24      else false;
    1.25 @@ -934,8 +934,8 @@
    1.26    (if is_copy_named_generating p
    1.27     then (*WN051014 kept strange old code ...*)
    1.28         let fun sel (_,_,d,ts) = comp_ts (d, ts) 
    1.29 -	   val cy' = (implode o (drop_last_n 3) o explode o free2str) t
    1.30 -	   val ext = (last_elem o drop_last o explode o free2str) t
    1.31 +	   val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t
    1.32 +	   val ext = (last_elem o drop_last o Symbol.explode o free2str) t
    1.33  	   val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
    1.34  	   val vals = map sel oris
    1.35  	   val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
    1.36 @@ -1334,7 +1334,7 @@
    1.37  	   (*TODO.WN03 pass error-msgs to the frontend..
    1.38               FIXME ..and dont abuse a tactic for that purpose*)
    1.39  	   ([(Tac msg,
    1.40 -	      Tac_ (theory "Pure", msg,msg,msg),
    1.41 +	      Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
    1.42  	      (e_pos', e_istate))], [], ptp) 
    1.43      end
    1.44