1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Tue Apr 14 12:39:26 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Tue Apr 14 15:56:15 2020 +0200
     1.3 @@ -28,9 +28,9 @@
     1.4  
     1.5    val term_of_num: typ -> int -> term
     1.6    val num_of_term: term -> int
     1.7 -  val int_of_str_opt: string -> int option
     1.8    val int_of_str: string -> int
     1.9    val isastr_of_int: int -> string
    1.10 +  val int_opt_of_string: string -> int option  (* belongs to TermC *)
    1.11  
    1.12    val isalist2list: term -> term list
    1.13    val list2isalist: typ -> term list -> term
    1.14 @@ -235,13 +235,13 @@
    1.15    else string_of_int n;
    1.16  val int_of_str = Value.parse_int;
    1.17  
    1.18 -val int_of_str_opt = ThmC_Def.int_of_str_opt
    1.19 +val int_opt_of_string = ThmC_Def.int_opt_of_string
    1.20  
    1.21 -fun is_num' str = case int_of_str_opt str of SOME _ => true | NONE => false;
    1.22 +fun is_num' str = case int_opt_of_string str of SOME _ => true | NONE => false;
    1.23  fun is_num (Free (s, _)) = if is_num' s then true else false | is_num _ = false;
    1.24  fun term_of_num ntyp n = Free (str_of_int n, ntyp);
    1.25  fun num_of_term (t as (Free (istr, _))) = 
    1.26 -    (case int_of_str_opt istr of SOME i => i | NONE => raise TERM ("num_of_term: NOT int ", [t]))
    1.27 +    (case int_opt_of_string istr of SOME i => i | NONE => raise TERM ("num_of_term: NOT int ", [t]))
    1.28    | num_of_term t = raise TERM ("num_of_term: NOT Free ", [t])
    1.29  
    1.30  fun is_const (Const _) = true | is_const _ = false;
    1.31 @@ -437,7 +437,7 @@
    1.32    end;
    1.33  
    1.34  (** transform binary numeralsstrings **)
    1.35 -val numbers_to_string = ThmC_Def.numbers_to_string
    1.36 +val numbers_to_string = ThmC_Def.num_to_Free
    1.37  val uminus_to_string = ThmC_Def.uminus_to_string
    1.38  
    1.39  fun mk_Free (s,T) = Free (s, T);
    1.40 @@ -507,11 +507,11 @@
    1.41  (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation
    1.42    WN130613 probably compare to 
    1.43    http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*)
    1.44 -fun parse_patt thy str =
    1.45 -  (thy, str) |>> ThyC.thy2ctxt 
    1.46 -             |-> Proof_Context.read_term_pattern
    1.47 -             |> numbers_to_string (*TODO drop*)
    1.48 -             |> typ_a2real;       (*TODO drop*)
    1.49 +fun parse_patt thy str = (thy, str)
    1.50 +  |>> ThyC.thy2ctxt 
    1.51 +  |-> Proof_Context.read_term_pattern
    1.52 +  |> numbers_to_string (*TODO drop*)
    1.53 +  |> typ_a2real;       (*TODO drop*)
    1.54  fun str2term str = parse_patt (ThyC.Thy_Info_get_theory "Isac_Knowledge") str
    1.55  
    1.56  (* TODO decide with Test_Isac *)