src/Pure/Syntax/syn_trans.ML
changeset 12150 f83dc4202b78
parent 12122 7f8d88ed4f21
child 12785 27debaf2112d
equal deleted inserted replaced
12149:7cf8574102d5 12150:f83dc4202b78
   300       (asms as _ :: _ :: _, concl)
   300       (asms as _ :: _ :: _, concl)
   301         => Ast.Appl [Ast.Constant "_bigimpl", Ast.fold_ast "_asms" asms, concl]
   301         => Ast.Appl [Ast.Constant "_bigimpl", Ast.fold_ast "_asms" asms, concl]
   302     | _ => raise Match);
   302     | _ => raise Match);
   303 
   303 
   304 
   304 
       
   305 (* meta conjunction *)
       
   306 
       
   307 fun meta_conjunction_tr' (*"all"*)
       
   308       [Abs (_, _, Const ("==>", _) $
       
   309         (Const ("==>", _) $ A $ (Const ("==>", _) $ B $ (Const ("_aprop", _) $ Bound 0))) $
       
   310         (Const ("_aprop", _) $ Bound 0))] =
       
   311       if 0 mem_int Term.loose_bnos A orelse 0 mem_int Term.loose_bnos B then raise Match
       
   312       else Lexicon.const "_meta_conjunction" $ A $ B
       
   313   | meta_conjunction_tr' (*"all"*) ts = raise Match;
       
   314 
       
   315 
   305 (* type reflection *)
   316 (* type reflection *)
   306 
   317 
   307 fun type_tr' show_sorts (*"TYPE"*) (Type ("itself", [T])) ts =
   318 fun type_tr' show_sorts (*"TYPE"*) (Type ("itself", [T])) ts =
   308       Term.list_comb (Lexicon.const "_TYPE" $ TypeExt.term_of_typ show_sorts T, ts)
   319       Term.list_comb (Lexicon.const "_TYPE" $ TypeExt.term_of_typ show_sorts T, ts)
   309   | type_tr' _ _ _ = raise Match;
   320   | type_tr' _ _ _ = raise Match;
   352  ([("_constify", constify_ast_tr), ("_appl", appl_ast_tr), ("_applC", applC_ast_tr),
   363  ([("_constify", constify_ast_tr), ("_appl", appl_ast_tr), ("_applC", applC_ast_tr),
   353    ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), ("_bigimpl", bigimpl_ast_tr),
   364    ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), ("_bigimpl", bigimpl_ast_tr),
   354    ("_indexvar", indexvar_ast_tr)],
   365    ("_indexvar", indexvar_ast_tr)],
   355   [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
   366   [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
   356    ("_TYPE", type_tr), ("_DDDOT", dddot_tr), ("_K", k_tr)],
   367    ("_TYPE", type_tr), ("_DDDOT", dddot_tr), ("_K", k_tr)],
   357   []: (string * (term list -> term)) list,
   368   [("all", meta_conjunction_tr')],
   358   [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
   369   [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
   359    ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr')]);
   370    ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr')]);
   360 
   371 
   361 val pure_trfunsT =
   372 val pure_trfunsT =
   362   [("_mk_ofclass", mk_ofclass_tr'), ("TYPE", type_tr')];
   373   [("_mk_ofclass", mk_ofclass_tr'), ("TYPE", type_tr')];