src/CTT/CTT.ML
changeset 4440 9ed4098074bc
parent 3929 3553fcfa2c7e
child 9249 c71db8c28727
     1.1 --- a/src/CTT/CTT.ML	Fri Dec 19 09:58:42 1997 +0100
     1.2 +++ b/src/CTT/CTT.ML	Fri Dec 19 10:13:47 1997 +0100
     1.3 @@ -150,7 +150,7 @@
     1.4  fun mp_tac i = etac subst_prodE i  THEN  assume_tac i;
     1.5  
     1.6  (*"safe" when regarded as predicate calculus rules*)
     1.7 -val safe_brls = sort lessb 
     1.8 +val safe_brls = sort (make_ord lessb)
     1.9      [ (true,FE), (true,asm_rl), 
    1.10        (false,ProdI), (true,SumE), (true,PlusE) ];
    1.11