1.1 --- a/src/Tools/isac/Interpret/generate.sml	Mon Feb 06 07:10:35 2017 +0100
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Mon Feb 06 07:21:28 2017 +0100
     1.3 @@ -29,7 +29,7 @@
     1.4    val generate_inconsistent_rew : Selem.subs option * thm'' -> term -> Selem.istate * Proof.context ->
     1.5      Ctree.pos' -> Ctree.ctree -> Ctree.state (* for interface.sml *)
     1.6  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
     1.7 -  (*  NONE *)
     1.8 +  val tacis2str : taci list -> string
     1.9  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.10    (*  NONE *)
    1.11  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.12 @@ -38,11 +38,10 @@
    1.13    (* NONE *)
    1.14  end
    1.15  
    1.16 -(**)
    1.17  structure Generate(**): GENERATE_CALC_TREE(**) =
    1.18 -(**)
    1.19  struct
    1.20  open Ctree
    1.21 +
    1.22  (* initialize istate for Detail_Set *)
    1.23  fun init_istate (Tac.Rewrite_Set rls) t =
    1.24      (case assoc_rls rls of
    1.25 @@ -139,22 +138,6 @@
    1.26  | RefineKF of Stool.match list                                       (*<--*)
    1.27  | RefinedKF of (pblID * ((Stool.itm list) * ((bool * term) list)))   (*<--*)
    1.28  
    1.29 -fun inout2str End_Proof = "End_Proof"
    1.30 -  | inout2str (Error_  s) = "Error_ "^s
    1.31 -  | inout2str (FormKF (cellID, edit, indent, nest, ct')) =  
    1.32 -	       "FormKF ("^(string_of_int cellID)^","
    1.33 -	       ^(edit2str edit)^","^(string_of_int indent)^","
    1.34 -	       ^(nest2str nest)^",("
    1.35 -	       ^ct' ^")"
    1.36 -  | inout2str (PpcKF (cellID, edit, indent, nest, (pm,itemppc))) =
    1.37 -	       "PpcKF ("^(string_of_int cellID)^","
    1.38 -	       ^(edit2str edit)^","^(string_of_int indent)^","
    1.39 -	       ^(nest2str nest)^",("
    1.40 -	       ^(pblmet2str pm)^","^(Stool.itemppc2str itemppc)^"))"
    1.41 -  | inout2str (RefineKF ms)  = "RefineKF "^(Stool.matchs2str ms)
    1.42 -  | inout2str _ = error "inout2str: uncovered definition"
    1.43 -fun inouts2str ios = (strs2str' o (map inout2str)) ios
    1.44 -
    1.45  (*
    1.46    datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
    1.47  *)
    1.48 @@ -167,7 +150,7 @@
    1.49  
    1.50  fun mout2str (FormKF cterm') = "FormKF " ^ cterm'
    1.51    | mout2str (PpcKF  (pm, itemppc)) = "PpcKF (" ^ pblmet2str pm ^ "," ^ Stool.itemppc2str itemppc ^ ")"
    1.52 -  | mout2str (RefinedKF  (pblID, ls)) = "mout2str: RefinedKF not impl."
    1.53 +  | mout2str (RefinedKF  (_, _)) = "mout2str: RefinedKF not impl."
    1.54    | mout2str (Error'  str) = "Error' " ^ str
    1.55    | mout2str (EmptyMout    ) = "EmptyMout"
    1.56