1.1 --- a/src/Tools/isac/Knowledge/InsSort.thy	Tue Feb 06 15:13:08 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy	Tue Feb 06 15:16:43 2018 +0100
     1.3 @@ -27,7 +27,7 @@
     1.4  where
     1.5  sort_deff: "sort xs = xfoldr ins xs {|| ||}"
     1.6  print_theorems
     1.7 -thm sort_def  (* InsSort.sort \<equiv> sort_sumC *)
     1.8 +(* thm sort_def  InsSort.sort \<equiv> sort_sumC *)
     1.9  thm sort_deff (* InsSort.sort ?xs = foldr ins ?xs [] *)
    1.10  
    1.11  (* access to definitions from ML *)