src/Tools/isac/BaseDefinitions/Know_Store.thy
changeset 59902 e7910a62eaf2
parent 59897 8cba439d0454
child 59903 5037ca1b112b
     1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Apr 22 11:06:48 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Apr 22 11:23:30 2020 +0200
     1.3 @@ -234,7 +234,7 @@
     1.4  (* we avoid term_to_string''' defined later *)
     1.5  fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =
     1.6    "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
     1.7 -  (Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.spec2str s ^ ")";
     1.8 +  (Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.to_string s ^ ")";
     1.9  
    1.10  fun count_kestore_ptyps [] = 0
    1.11    | count_kestore_ptyps ((Store.Node (_, _, ps)) :: ps') =