1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Wed Aug 24 17:25:40 2016 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Wed Aug 24 17:27:54 2016 +0200
     1.3 @@ -316,10 +316,6 @@
     1.4      if id = #1 p then SOME p else seek_ppc id ppc;
     1.5  
     1.6  
     1.7 -
     1.8 -(*---------------------------------------------(3) nach ptyps.sml 23.3.02*)
     1.9 -
    1.10 -
    1.11  datatype appl = Appl of tac_ | Notappl of string;
    1.12  
    1.13  fun ppc2list ({Given=gis,Where=whs,Find=fis,
    1.14 @@ -786,7 +782,7 @@
    1.15  
    1.16  (** make oris from args of the stac SubProblem and from pbt **)
    1.17  (* can this formal argument (of a model-pattern) be omitted in the arg-list
    1.18 -   of a SubProblem ? see ME/ptyps.sml 'type met ' *)
    1.19 +   of a SubProblem ? see calcelems.sml 'type met ' *)
    1.20  fun is_copy_named_idstr str =
    1.21      case (rev o Symbol.explode) str of
    1.22  	"'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode)) 

     2.1 --- a/src/Tools/isac/Interpret/ptyps.sml	Wed Aug 24 17:25:40 2016 +0200
     2.2 +++ b/src/Tools/isac/Interpret/ptyps.sml	Wed Aug 24 17:27:54 2016 +0200
     2.3 @@ -1,9 +1,6 @@
     2.4  (* the problems and methods as stored in hierarchies
     2.5     author Walther Neuper 1998, Mathias Lehnfeld
     2.6     (c) due to copyright terms
     2.7 -
     2.8 -use"ME/ptyps.sml";
     2.9 -use"ptyps.sml";
    2.10  *)
    2.11  
    2.12  (*-----------------------------------------vvv-(1) aus modspec.sml 23.3.02*)

     3.1 --- a/test/Tools/isac/Test_Some.thy	Wed Aug 24 17:25:40 2016 +0200
     3.2 +++ b/test/Tools/isac/Test_Some.thy	Wed Aug 24 17:27:54 2016 +0200
     3.3 @@ -15,10 +15,12 @@
     3.4    declare [[show_sorts]]            
     3.5    find_theorems "?a <= ?a"
     3.6    
     3.7 +  print_theorems
     3.8    print_facts
     3.9    print_statement ""
    3.10    print_theory
    3.11 -ML_command \<open>Pretty.writeln prt\<close>
    3.12 +  ML_command \<open>Pretty.writeln prt\<close>
    3.13 +  declare [[ML_print_depth = 999]]
    3.14  *}
    3.15  ML {*
    3.16  (*========== inhibit exn WN130909 TODO =========================================================