TFL/tfl.sml
changeset 4252 d5ccc8321e1e
parent 4221 ed0f67fb458b
child 4857 cf554f1c65be
equal deleted inserted replaced
4251:f6bd8332eb32 4252:d5ccc8321e1e
   333 				      quote Name}
   333 				      quote Name}
   334 		    else Name ^ "_def"
   334 		    else Name ^ "_def"
   335      val wfrec_R_M =  map_term_types poly_tvars 
   335      val wfrec_R_M =  map_term_types poly_tvars 
   336 	                  (wfrec $ map_term_types poly_tvars R) 
   336 	                  (wfrec $ map_term_types poly_tvars R) 
   337 	              $ functional
   337 	              $ functional
   338      val (_, def_term, _) = 
   338      val (def_term, _) = 
   339 	 Sign.infer_types (sign_of thy) (K None) (K None) [] false
   339 	 Sign.infer_types (sign_of thy) (K None) (K None) [] false
   340 	       ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M], 
   340 	       ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M], 
   341 		propT)
   341 		propT)
   342   in  PureThy.add_store_defs_i [(def_name, def_term)] thy  end
   342   in  PureThy.add_store_defs_i [(def_name, def_term)] thy  end
   343 end;
   343 end;