src/Pure/thm.ML
changeset 4439 02730662e446
parent 4397 7f760385a3a5
child 4589 543e867efe40
     1.1 --- a/src/Pure/thm.ML	Fri Dec 19 09:58:03 1997 +0100
     1.2 +++ b/src/Pure/thm.ML	Fri Dec 19 09:58:42 1997 +0100
     1.3 @@ -1524,7 +1524,7 @@
     1.4      prems = prems, mk_rews = mk_rews, termless = termless};
     1.5  
     1.6  val empty_mss =
     1.7 -  mk_mss (Net.empty, [], Net.empty, [], [], K [], Logic.termless);
     1.8 +  mk_mss (Net.empty, [], Net.empty, [], [], K [], Term.termless);
     1.9  
    1.10  
    1.11