src/HOL/thy_syntax.ML
changeset 6035 c041fc54ab4c
parent 5716 a3d2a6b6693e
child 6103 36f272ea9413
equal deleted inserted replaced
6034:96ac04a17c56 6035:c041fc54ab4c
    43 fun inductive_decl coind =
    43 fun inductive_decl coind =
    44   let
    44   let
    45     fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
    45     fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
    46       if Syntax.is_identifier s then "op " ^ s else "_";
    46       if Syntax.is_identifier s then "op " ^ s else "_";
    47     fun mk_params (((recs, ipairs), monos), con_defs) =
    47     fun mk_params (((recs, ipairs), monos), con_defs) =
    48       let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs)
    48       let val big_rec_name = space_implode "_" (map (scan_to_id o strip_quotes) recs)
    49           and srec_tms = mk_list recs
    49           and srec_tms = mk_list recs
    50           and sintrs   = mk_big_list (map snd ipairs)
    50           and sintrs   = mk_big_list (map snd ipairs)
    51       in
    51       in
    52         ";\n\n\
    52         ";\n\n\
    53         \local\n\
    53         \local\n\
   204 (** rec: interface to Slind's TFL **)
   204 (** rec: interface to Slind's TFL **)
   205 
   205 
   206 
   206 
   207 (*fname: name of function being defined; rel: well-founded relation*)
   207 (*fname: name of function being defined; rel: well-founded relation*)
   208 fun mk_rec_decl ((((fname, rel), congs), ss), axms) =
   208 fun mk_rec_decl ((((fname, rel), congs), ss), axms) =
   209   let val fid = trim fname
   209   let val fid = strip_quotes fname
   210       val intrnl_name = fid ^ "_Intrnl"
   210       val intrnl_name = fid ^ "_Intrnl"
   211   in
   211   in
   212 	 (";\n\n\
   212 	 (";\n\n\
   213           \val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
   213           \val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
   214           \val (thy, pats_" ^ intrnl_name ^ ") = Tfl.define thy " ^ 
   214           \val (thy, pats_" ^ intrnl_name ^ ") = Tfl.define thy " ^ 
   224           \    \t\t  (thy, (" ^ quote fid ^ ", pats_" ^ intrnl_name ^ "))\n\
   224           \    \t\t  (thy, (" ^ quote fid ^ ", pats_" ^ intrnl_name ^ "))\n\
   225           \  end;\n\
   225           \  end;\n\
   226           \val pats_" ^ intrnl_name ^ " = ();\n")
   226           \val pats_" ^ intrnl_name ^ " = ();\n")
   227   end;
   227   end;
   228 
   228 
   229 val rec_decl = (name -- string -- 
   229 val rec_decl = 
   230 		optional ("congs" $$-- string >> trim) "[]" -- 
   230     (name -- string -- 
   231 		optional ("simpset" $$-- string >> trim) "simpset()" -- 
   231      optional ("congs" $$-- string >> strip_quotes) "[]" -- 
   232 		repeat1 string >> mk_rec_decl) ;
   232      optional ("simpset" $$-- string >> strip_quotes) "simpset()" -- 
       
   233      repeat1 string >> mk_rec_decl) ;
   233 
   234 
   234 
   235 
   235 
   236 
   236 (** augment thy syntax **)
   237 (** augment thy syntax **)
   237 
   238