src/Pure/Isar/proof_context.ML
changeset 39508 dfacdb01e1ec
parent 39507 839873937ddd
child 39557 fe5722fce758
equal deleted inserted replaced
39507:839873937ddd 39508:dfacdb01e1ec
   583   in T end;
   583   in T end;
   584 
   584 
   585 
   585 
   586 local
   586 local
   587 
   587 
   588 structure Allow_Dummies = Proof_Data(type T = bool fun init _ = false);
   588 val dummies = Config.bool (Config.declare "ProofContext.dummies" (K (Config.Bool false)));
   589 
   589 
   590 fun check_dummies ctxt t =
   590 fun check_dummies ctxt t =
   591   if Allow_Dummies.get ctxt then t
   591   if Config.get ctxt dummies then t
   592   else Term.no_dummy_patterns t handle TERM _ => error "Illegal dummy pattern(s) in term";
   592   else Term.no_dummy_patterns t handle TERM _ => error "Illegal dummy pattern(s) in term";
   593 
   593 
   594 fun prepare_dummies ts = #1 (fold_map Term.replace_dummy_patterns ts 1);
   594 fun prepare_dummies ts = #1 (fold_map Term.replace_dummy_patterns ts 1);
   595 
   595 
   596 in
   596 in
   597 
   597 
   598 val allow_dummies = Allow_Dummies.put true;
   598 val allow_dummies = Config.put dummies true;
   599 
   599 
   600 fun prepare_patterns ctxt =
   600 fun prepare_patterns ctxt =
   601   let val Mode {pattern, ...} = get_mode ctxt in
   601   let val Mode {pattern, ...} = get_mode ctxt in
   602     Type_Infer.fixate ctxt #>
   602     Type_Infer.fixate ctxt #>
   603     pattern ? Variable.polymorphic ctxt #>
   603     pattern ? Variable.polymorphic ctxt #>